Theorem sbc2rex

Description: Exchange a substitution with two existentials. (Contributed by Stefan O'Rear, 11-Oct-2014) (Revised by NM, 24-Aug-2018)

	Ref	Expression
Assertion	sbc2rex	$$⊢\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$$

Proof

Step	Hyp	Ref	Expression
1		sbcrex	$$⊢\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$$
2		sbcrex	$$⊢\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\exists c\in C\phi \leftrightarrow \exists c\in C\underset{\dot{}}{[}A/a\underset{\dot{}}{]}\phi$$
3	2	rexbii	$$⊢\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$$
4	1 3	bitri	$$⊢\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$$