Axiom ax-subse1 220

Assertion

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

Detailed syntax breakdown of Axiom ax-subse1

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

This axiom is referenced by: (None)