Definition df-vnab 272

Description: Definition of simple nilads.

Assertion

Ref	Expression
df-vnab	⊦ {νx | 𝜑} = {r | νx[r ≪ x] 𝜑}

Detailed syntax breakdown of Definition df-vnab

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 var x
3	1, 2	nvnab 271	. 2 nilad {νx | 𝜑}
4		vr	. . . . . 6 var r
5	4	nvar 203	. . . . 5 nilad r
6	2	nvar 203	. . . . 5 nilad x
7	1, 5, 6	wse 204	. . . 4 wff [r ≪ x] 𝜑
8	7, 2	wnu 206	. . 3 wff νx[r ≪ x] 𝜑
9	8, 4	nnab 266	. 2 nilad {r | νx[r ≪ x] 𝜑}
10	3, 9	weq 246	1 wff {νx | 𝜑} = {r | νx[r ≪ x] 𝜑}

This definition is referenced by: (None)