Theorem sbccom2f

Description: Commutative law for double class substitution, with nonfree variable condition. (Contributed by Giovanni Mascellani, 31-May-2019)

	Ref	Expression
Hypotheses	sbccom2f.1	$$⊢A\in \mathrm{V}$$
	sbccom2f.2	$$⊢\underset{\_}{Ⅎ}yA$$
Assertion	sbccom2f	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}⦋A/x⦌B/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$

Proof

Step	Hyp	Ref	Expression
1		sbccom2f.1	$$⊢A\in \mathrm{V}$$
2		sbccom2f.2	$$⊢\underset{\_}{Ⅎ}yA$$
3		sbcco	$$⊢\underset{\dot{}}{[}B/z\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi$$
4	3	bicomi	$$⊢\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}B/z\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi$$
5	4	sbcbii	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/z\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi$$
6	1	sbccom2	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/z\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}⦋A/x⦌B/z\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi$$
7		vex	$$⊢z\in \mathrm{V}$$
8	7	sbccom2	$$⊢\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}⦋z/y⦌A/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi$$
9	7 2	csbgfi	$$⊢⦋z/y⦌A=A$$
10		dfsbcq	$$⊢⦋z/y⦌A=A\to \left(\underset{\dot{}}{[}⦋z/y⦌A/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right)$$
11	9 10	ax-mp	$$⊢\underset{\dot{}}{[}⦋z/y⦌A/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi$$
12	8 11	bitri	$$⊢\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi$$
13	12	bicomi	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}z/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
14	13	sbcbii	$$⊢\underset{\dot{}}{[}⦋A/x⦌B/z\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}⦋A/x⦌B/z\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
15		sbcco	$$⊢\underset{\dot{}}{[}⦋A/x⦌B/z\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}⦋A/x⦌B/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
16	14 15	bitri	$$⊢\underset{\dot{}}{[}⦋A/x⦌B/z\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}⦋A/x⦌B/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
17	5 6 16	3bitri	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}⦋A/x⦌B/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$