Theorem sbccomieg

Description: Commute two explicit substitutions, using an implicit substitution to rewrite the exiting substitution. (Contributed by Stefan O'Rear, 11-Oct-2014) (Revised by Mario Carneiro, 11-Dec-2016)

	Ref	Expression
Hypothesis	sbccomieg.1	$$⊢a=A\to B=C$$
Assertion	sbccomieg	$$⊢\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\underset{\dot{}}{[}B/b\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}C/b\underset{\dot{}}{]}\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\phi$$

Proof

Step	Hyp	Ref	Expression
1		sbccomieg.1	$$⊢a=A\to B=C$$
2		sbcex	$$⊢\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\underset{\dot{}}{[}B/b\underset{\dot{}}{]}\phi \to A\in \mathrm{V}$$
3		spesbc	$$⊢\underset{\dot{}}{[}C/b\underset{\dot{}}{]}\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\phi \to \exists b\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\phi$$
4		sbcex	$$⊢\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\phi \to A\in \mathrm{V}$$
5	4	exlimiv	$$⊢\exists b\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\phi \to A\in \mathrm{V}$$
6	3 5	syl	$$⊢\underset{\dot{}}{[}C/b\underset{\dot{}}{]}\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\phi \to A\in \mathrm{V}$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}aC$$
8		nfsbc1v	$$⊢Ⅎa\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\phi$$
9	7 8	nfsbcw	$$⊢Ⅎa\underset{\dot{}}{[}C/b\underset{\dot{}}{]}\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\phi$$
10		sbceq1a	$$⊢a=A\to \left(\phi \leftrightarrow \underset{\dot{}}{[}A/a\underset{\dot{}}{]}\phi \right)$$
11	1 10	sbceqbid	$$⊢a=A\to \left(\underset{\dot{}}{[}B/b\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}C/b\underset{\dot{}}{]}\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\phi \right)$$
12	9 11	sbciegf	$$⊢A\in \mathrm{V}\to \left(\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\underset{\dot{}}{[}B/b\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}C/b\underset{\dot{}}{]}\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\phi \right)$$
13	2 6 12	pm5.21nii	$$⊢\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\underset{\dot{}}{[}B/b\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}C/b\underset{\dot{}}{]}\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\phi$$