Theorem sbcrexgOLD

Description: Interchange class substitution and restricted existential quantifier. (Contributed by NM, 15-Nov-2005) (Proof shortened by Andrew Salmon, 29-Jun-2011) Obsolete as of 18-Aug-2018. Use sbcrex instead. (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	sbcrexgOLD	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\in B\phi \leftrightarrow \exists y\in B\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		dfsbcq2	$$⊢z=A\to \left(\left[z/x\right]\exists y\in B\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\in B\phi \right)$$
2		dfsbcq2	$$⊢z=A\to \left(\left[z/x\right]\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
3	2	rexbidv	$$⊢z=A\to \left(\exists y\in B\left[z/x\right]\phi \leftrightarrow \exists y\in B\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}xB$$
5		nfs1v	$$⊢Ⅎx\left[z/x\right]\phi$$
6	4 5	nfrexw	$$⊢Ⅎx\exists y\in B\left[z/x\right]\phi$$
7		sbequ12	$$⊢x=z\to \left(\phi \leftrightarrow \left[z/x\right]\phi \right)$$
8	7	rexbidv	$$⊢x=z\to \left(\exists y\in B\phi \leftrightarrow \exists y\in B\left[z/x\right]\phi \right)$$
9	6 8	sbie	$$⊢\left[z/x\right]\exists y\in B\phi \leftrightarrow \exists y\in B\left[z/x\right]\phi$$
10	1 3 9	vtoclbg	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\in B\phi \leftrightarrow \exists y\in B\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$