Axiom ax-subnu1 225

Assertion

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

Detailed syntax breakdown of Axiom ax-subnu1

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

This axiom is referenced by: (None)