Axiom ax-subse3 222

Assertion

Ref	Expression
ax-subse3	⊦ ([x ≔ y] [u ≪ v] 𝜑 ⧟ [u ≪ v] [x ≔ y] 𝜑)

Distinct variable groups:   u,x   u,y   v,x   v,y

Detailed syntax breakdown of Axiom ax-subse3

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

This axiom is referenced by: (None)