Theorem dfnab3 270

Description: Write to a nilad.

Assertion

Ref	Expression
dfnab3	⊦ ([{x | 𝜑} ≪ Y] 𝜓 ⧟ (𝜑 ⊗ [x ≫ a] [a ≪ Y] 𝜓))

Distinct variable groups:   𝜑,a   𝜓,a   a,Y   a,x

Proof of Theorem dfnab3

Step	Hyp	Ref	Expression

Syntax hints:   ⧟ wlb 55   ⊗ wmc 105  nvar 203  [wse 204  [wre 205  {nnab 266

 WARNING: This theorem has an incomplete proof.

This theorem is referenced by: (None)