Axiom ax-subse2 221

Assertion

Ref	Expression
ax-subse2	⊦ ([x ≔ y] [a ≪ x] 𝜑 ⧟ [x ≔ y] [a ≪ y] 𝜑)

Detailed syntax breakdown of Axiom ax-subse2

Step	Hyp	Ref	Expression
1		wph	. . . 4 wff 𝜑
2		va	. . . . 5 var a
3	2	nvar 203	. . . 4 nilad a
4		vx	. . . . 5 var x
5	4	nvar 203	. . . 4 nilad x
6	1, 3, 5	wse 204	. . 3 wff [a ≪ x] 𝜑
7		vy	. . . 4 var y
8	7	nvar 203	. . 3 nilad y
9	6, 4, 8	wsub 207	. 2 wff [x ≔ y] [a ≪ x] 𝜑
10	1, 3, 8	wse 204	. . 3 wff [a ≪ y] 𝜑
11	10, 4, 8	wsub 207	. 2 wff [x ≔ y] [a ≪ y] 𝜑
12	9, 11	wlb 55	1 wff ([x ≔ y] [a ≪ x] 𝜑 ⧟ [x ≔ y] [a ≪ y] 𝜑)

This axiom is referenced by: (None)