Theorem sbccom2fi

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

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

Proof

Step	Hyp	Ref	Expression
1		sbccom2fi.1	$$⊢A\in \mathrm{V}$$
2		sbccom2fi.2	$$⊢\underset{\_}{Ⅎ}yA$$
3		sbccom2fi.3	$$⊢⦋A/x⦌B=C$$
4		sbccom2fi.4	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \psi$$
5	1 2	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$$
6		dfsbcq	$$⊢⦋A/x⦌B=C\to \left(\underset{\dot{}}{[}⦋A/x⦌B/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}C/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
7	3 6	ax-mp	$$⊢\underset{\dot{}}{[}⦋A/x⦌B/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}C/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
8	4	sbcbii	$$⊢\underset{\dot{}}{[}C/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}C/y\underset{\dot{}}{]}\psi$$
9	5 7 8	3bitri	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}C/y\underset{\dot{}}{]}\psi$$