Theorem dfnab1 268

Description: df-nab 267 also works on nilads.

Assertion

Ref	Expression
dfnab1	⊦ ([X ≪ {y | 𝜑}] 𝜓 ⧟ (𝜑 ⊗ [y ≫ a] [X ≪ a] 𝜓))

Distinct variable groups:   𝜑,a   𝜓,a   a,X   a,y

Proof of Theorem dfnab1

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)