Theorem csbcom2fi

Description: Commutative law for double class substitution in a class, with nonfree variable condition and in inference form. (Contributed by Giovanni Mascellani, 4-Jun-2019)

	Ref	Expression
Hypotheses	csbcom2fi.1	$$⊢A\in \mathrm{V}$$
	csbcom2fi.2	$$⊢\underset{\_}{Ⅎ}yA$$
	csbcom2fi.3	$$⊢⦋A/x⦌B=C$$
	csbcom2fi.4	$$⊢⦋A/x⦌D=E$$
Assertion	csbcom2fi	$$⊢⦋A/x⦌⦋B/y⦌D=⦋C/y⦌E$$

Proof

Step	Hyp	Ref	Expression
1		csbcom2fi.1	$$⊢A\in \mathrm{V}$$
2		csbcom2fi.2	$$⊢\underset{\_}{Ⅎ}yA$$
3		csbcom2fi.3	$$⊢⦋A/x⦌B=C$$
4		csbcom2fi.4	$$⊢⦋A/x⦌D=E$$
5		df-csb	$$⊢⦋A/x⦌⦋B/y⦌D=\left\{z|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in ⦋B/y⦌D\right\}$$
6	5	eqabri	$$⊢z\in ⦋A/x⦌⦋B/y⦌D\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in ⦋B/y⦌D$$
7		df-csb	$$⊢⦋B/y⦌D=\left\{z|\underset{\dot{}}{[}B/y\underset{\dot{}}{]}z\in D\right\}$$
8	7	eqabri	$$⊢z\in ⦋B/y⦌D\leftrightarrow \underset{\dot{}}{[}B/y\underset{\dot{}}{]}z\in D$$
9	8	sbcbii	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in ⦋B/y⦌D\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}z\in D$$
10	6 9	bitri	$$⊢z\in ⦋A/x⦌⦋B/y⦌D\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}z\in D$$
11		df-csb	$$⊢⦋A/x⦌D=\left\{z|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in D\right\}$$
12	11	eqabri	$$⊢z\in ⦋A/x⦌D\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in D$$
13	4	eleq2i	$$⊢z\in ⦋A/x⦌D\leftrightarrow z\in E$$
14	12 13	bitr3i	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in D\leftrightarrow z\in E$$
15	1 2 3 14	sbccom2fi	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}z\in D\leftrightarrow \underset{\dot{}}{[}C/y\underset{\dot{}}{]}z\in E$$
16		sbcel2	$$⊢\underset{\dot{}}{[}C/y\underset{\dot{}}{]}z\in E\leftrightarrow z\in ⦋C/y⦌E$$
17	10 15 16	3bitri	$$⊢z\in ⦋A/x⦌⦋B/y⦌D\leftrightarrow z\in ⦋C/y⦌E$$
18	17	eqriv	$$⊢⦋A/x⦌⦋B/y⦌D=⦋C/y⦌E$$