Theorem sbcrext

Description: Interchange class substitution and restricted existential quantifier. (Contributed by NM, 1-Mar-2008) (Proof shortened by Mario Carneiro, 13-Oct-2016) (Revised by NM, 18-Aug-2018) (Proof shortened by JJ, 7-Jul-2021)

	Ref	Expression
Assertion	sbcrext	$$⊢\underset{\_}{Ⅎ}yA\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		sbcex	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\in B\phi \to A\in \mathrm{V}$$
2	1	a1i	$$⊢\underset{\_}{Ⅎ}yA\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\in B\phi \to A\in \mathrm{V}\right)$$
3		nfnfc1	$$⊢Ⅎy\underset{\_}{Ⅎ}yA$$
4		id	$$⊢\underset{\_}{Ⅎ}yA\to \underset{\_}{Ⅎ}yA$$
5		nfcvd	$$⊢\underset{\_}{Ⅎ}yA\to \underset{\_}{Ⅎ}y\mathrm{V}$$
6	4 5	nfeld	$$⊢\underset{\_}{Ⅎ}yA\to ℲyA\in \mathrm{V}$$
7		sbcex	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \to A\in \mathrm{V}$$
8	7	2a1i	$$⊢\underset{\_}{Ⅎ}yA\to \left(y\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \to A\in \mathrm{V}\right)\right)$$
9	3 6 8	rexlimd2	$$⊢\underset{\_}{Ⅎ}yA\to \left(\exists y\in B\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \to A\in \mathrm{V}\right)$$
10		sbcng	$$⊢A\in \mathrm{V}\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\neg \forall y\in B\neg \phi \leftrightarrow \neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\in B\neg \phi \right)$$
11	10	adantl	$$⊢\left(\underset{\_}{Ⅎ}yA\wedge A\in \mathrm{V}\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\neg \forall y\in B\neg \phi \leftrightarrow \neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\in B\neg \phi \right)$$
12		sbcralt	$$⊢\left(A\in \mathrm{V}\wedge \underset{\_}{Ⅎ}yA\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\in B\neg \phi \leftrightarrow \forall y\in B\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\neg \phi \right)$$
13	12	ancoms	$$⊢\left(\underset{\_}{Ⅎ}yA\wedge A\in \mathrm{V}\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\in B\neg \phi \leftrightarrow \forall y\in B\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\neg \phi \right)$$
14	3 6	nfan1	$$⊢Ⅎy\left(\underset{\_}{Ⅎ}yA\wedge A\in \mathrm{V}\right)$$
15		sbcng	$$⊢A\in \mathrm{V}\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\neg \phi \leftrightarrow \neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
16	15	adantl	$$⊢\left(\underset{\_}{Ⅎ}yA\wedge A\in \mathrm{V}\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\neg \phi \leftrightarrow \neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
17	14 16	ralbid	$$⊢\left(\underset{\_}{Ⅎ}yA\wedge A\in \mathrm{V}\right)\to \left(\forall y\in B\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\neg \phi \leftrightarrow \forall y\in B\neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
18	13 17	bitrd	$$⊢\left(\underset{\_}{Ⅎ}yA\wedge A\in \mathrm{V}\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\in B\neg \phi \leftrightarrow \forall y\in B\neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
19	18	notbid	$$⊢\left(\underset{\_}{Ⅎ}yA\wedge A\in \mathrm{V}\right)\to \left(\neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\in B\neg \phi \leftrightarrow \neg \forall y\in B\neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
20	11 19	bitrd	$$⊢\left(\underset{\_}{Ⅎ}yA\wedge A\in \mathrm{V}\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\neg \forall y\in B\neg \phi \leftrightarrow \neg \forall y\in B\neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
21		dfrex2	$$⊢\exists y\in B\phi \leftrightarrow \neg \forall y\in B\neg \phi$$
22	21	sbcbii	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\in B\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\neg \forall y\in B\neg \phi$$
23		dfrex2	$$⊢\exists y\in B\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \neg \forall y\in B\neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
24	20 22 23	3bitr4g	$$⊢\left(\underset{\_}{Ⅎ}yA\wedge A\in \mathrm{V}\right)\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)$$
25	24	ex	$$⊢\underset{\_}{Ⅎ}yA\to \left(A\in \mathrm{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)\right)$$
26	2 9 25	pm5.21ndd	$$⊢\underset{\_}{Ⅎ}yA\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)$$