Theorem sbc2rexgOLD

Description: Exchange a substitution with two existentials. (Contributed by Stefan O'Rear, 11-Oct-2014) Obsolete as of 24-Aug-2018. Use csbov123 instead. (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	sbc2rexgOLD	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\exists b\in B\exists c\in C\phi \leftrightarrow \exists b\in B\exists c\in C\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		elex	$$⊢A\in V\to A\in \mathrm{V}$$
2		sbcrexgOLD	$$⊢A\in \mathrm{V}\to \left(\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\exists b\in B\exists c\in C\phi \leftrightarrow \exists b\in B\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\exists c\in C\phi \right)$$
3		sbcrexgOLD	$$⊢A\in \mathrm{V}\to \left(\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\exists c\in C\phi \leftrightarrow \exists c\in C\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\phi \right)$$
4	3	rexbidv	$$⊢A\in \mathrm{V}\to \left(\exists b\in B\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\exists c\in C\phi \leftrightarrow \exists b\in B\exists c\in C\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\phi \right)$$
5	2 4	bitrd	$$⊢A\in \mathrm{V}\to \left(\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\exists b\in B\exists c\in C\phi \leftrightarrow \exists b\in B\exists c\in C\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\phi \right)$$
6	1 5	syl	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\exists b\in B\exists c\in C\phi \leftrightarrow \exists b\in B\exists c\in C\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\phi \right)$$