Theorem csbcom

Description: Commutative law for double substitution into a class. (Contributed by NM, 14-Nov-2005) (Revised by NM, 18-Aug-2018)

	Ref	Expression
Assertion	csbcom	$$⊢⦋A/x⦌⦋B/y⦌C=⦋B/y⦌⦋A/x⦌C$$

Proof

Step	Hyp	Ref	Expression
1		sbccom	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}z\in C\leftrightarrow \underset{\dot{}}{[}B/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in C$$
2		sbcel2	$$⊢\underset{\dot{}}{[}B/y\underset{\dot{}}{]}z\in C\leftrightarrow z\in ⦋B/y⦌C$$
3	2	sbcbii	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}z\in C\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in ⦋B/y⦌C$$
4		sbcel2	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in C\leftrightarrow z\in ⦋A/x⦌C$$
5	4	sbcbii	$$⊢\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in C\leftrightarrow \underset{\dot{}}{[}B/y\underset{\dot{}}{]}z\in ⦋A/x⦌C$$
6	1 3 5	3bitr3i	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in ⦋B/y⦌C\leftrightarrow \underset{\dot{}}{[}B/y\underset{\dot{}}{]}z\in ⦋A/x⦌C$$
7		sbcel2	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in ⦋B/y⦌C\leftrightarrow z\in ⦋A/x⦌⦋B/y⦌C$$
8		sbcel2	$$⊢\underset{\dot{}}{[}B/y\underset{\dot{}}{]}z\in ⦋A/x⦌C\leftrightarrow z\in ⦋B/y⦌⦋A/x⦌C$$
9	6 7 8	3bitr3i	$$⊢z\in ⦋A/x⦌⦋B/y⦌C\leftrightarrow z\in ⦋B/y⦌⦋A/x⦌C$$
10	9	eqriv	$$⊢⦋A/x⦌⦋B/y⦌C=⦋B/y⦌⦋A/x⦌C$$