Axiom ax-subnu2 226

Assertion

Ref	Expression
ax-subnu2	⊦ ([x ≔ y] νu𝜑 ⧟ νu[x ≔ y] 𝜑)

Distinct variable groups:   u,x   u,y

Detailed syntax breakdown of Axiom ax-subnu2

Step	Hyp	Ref	Expression
1		wph	. . . 4 wff 𝜑
2		vu	. . . 4 var u
3	1, 2	wnu 206	. . 3 wff νu𝜑
4		vx	. . 3 var x
5		vy	. . . 4 var y
6	5	nvar 203	. . 3 nilad y
7	3, 4, 6	wsub 207	. 2 wff [x ≔ y] νu𝜑
8	1, 4, 6	wsub 207	. . 3 wff [x ≔ y] 𝜑
9	8, 2	wnu 206	. 2 wff νu[x ≔ y] 𝜑
10	7, 9	wlb 55	1 wff ([x ≔ y] νu𝜑 ⧟ νu[x ≔ y] 𝜑)

This axiom is referenced by: (None)