Definition df-nsub 278

Description: The proper substitution of x with Y in F.

Assertion

Ref	Expression
df-nsub	⊦ [x ≔ Y] F = {r | νa[x ≔ y] [F ≫ f] [r ≪ f] 1}

Distinct variable groups:   a,r,x   r,Y,a   r,F,a

Detailed syntax breakdown of Definition df-nsub

Step	Hyp	Ref	Expression
1		vx	. . 3 var x
2		nf	. . 3 nilad F
3		ny	. . 3 nilad Y
4	1, 2, 3	nsub 277	. 2 nilad [x ≔ Y] F
5		wone 103	. . . . . . 7 wff 1
6		vr	. . . . . . . 8 var r
7	6	nvar 203	. . . . . . 7 nilad r
8		vf	. . . . . . . 8 var f
9	8	nvar 203	. . . . . . 7 nilad f
10	5, 7, 9	wse 204	. . . . . 6 wff [r ≪ f] 1
11	10, 8, 2	wre 205	. . . . 5 wff [F ≫ f] [r ≪ f] 1
12		vy	. . . . . 6 var y
13	12	nvar 203	. . . . 5 nilad y
14	11, 1, 13	wsub 207	. . . 4 wff [x ≔ y] [F ≫ f] [r ≪ f] 1
15		va	. . . 4 var a
16	14, 15	wnu 206	. . 3 wff νa[x ≔ y] [F ≫ f] [r ≪ f] 1
17	16, 6	nnab 266	. 2 nilad {r | νa[x ≔ y] [F ≫ f] [r ≪ f] 1}
18	4, 17	weq 246	1 wff [x ≔ Y] F = {r | νa[x ≔ y] [F ≫ f] [r ≪ f] 1}

This definition is referenced by: (None)