Metamath Proof Explorer

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 
|- ( F/_ y A -> ( [. A / x ]. E. y e. B ph <-> E. y e. B [. A / x ]. ph ) )

Proof

Step Hyp Ref Expression
1 sbcex 
 |-  ( [. A / x ]. E. y e. B ph -> A e. _V )
2 1 a1i 
 |-  ( F/_ y A -> ( [. A / x ]. E. y e. B ph -> A e. _V ) )
3 nfnfc1 
 |-  F/ y F/_ y A
4 id 
 |-  ( F/_ y A -> F/_ y A )
5 nfcvd 
 |-  ( F/_ y A -> F/_ y _V )
6 4 5 nfeld 
 |-  ( F/_ y A -> F/ y A e. _V )
7 sbcex 
 |-  ( [. A / x ]. ph -> A e. _V )
8 7 2a1i 
 |-  ( F/_ y A -> ( y e. B -> ( [. A / x ]. ph -> A e. _V ) ) )
9 3 6 8 rexlimd2 
 |-  ( F/_ y A -> ( E. y e. B [. A / x ]. ph -> A e. _V ) )
10 sbcng 
 |-  ( A e. _V -> ( [. A / x ]. -. A. y e. B -. ph <-> -. [. A / x ]. A. y e. B -. ph ) )
11 10 adantl 
 |-  ( ( F/_ y A /\ A e. _V ) -> ( [. A / x ]. -. A. y e. B -. ph <-> -. [. A / x ]. A. y e. B -. ph ) )
12 sbcralt 
 |-  ( ( A e. _V /\ F/_ y A ) -> ( [. A / x ]. A. y e. B -. ph <-> A. y e. B [. A / x ]. -. ph ) )
13 12 ancoms 
 |-  ( ( F/_ y A /\ A e. _V ) -> ( [. A / x ]. A. y e. B -. ph <-> A. y e. B [. A / x ]. -. ph ) )
14 3 6 nfan1 
 |-  F/ y ( F/_ y A /\ A e. _V )
15 sbcng 
 |-  ( A e. _V -> ( [. A / x ]. -. ph <-> -. [. A / x ]. ph ) )
16 15 adantl 
 |-  ( ( F/_ y A /\ A e. _V ) -> ( [. A / x ]. -. ph <-> -. [. A / x ]. ph ) )
17 14 16 ralbid 
 |-  ( ( F/_ y A /\ A e. _V ) -> ( A. y e. B [. A / x ]. -. ph <-> A. y e. B -. [. A / x ]. ph ) )
18 13 17 bitrd 
 |-  ( ( F/_ y A /\ A e. _V ) -> ( [. A / x ]. A. y e. B -. ph <-> A. y e. B -. [. A / x ]. ph ) )
19 18 notbid 
 |-  ( ( F/_ y A /\ A e. _V ) -> ( -. [. A / x ]. A. y e. B -. ph <-> -. A. y e. B -. [. A / x ]. ph ) )
20 11 19 bitrd 
 |-  ( ( F/_ y A /\ A e. _V ) -> ( [. A / x ]. -. A. y e. B -. ph <-> -. A. y e. B -. [. A / x ]. ph ) )
21 dfrex2 
 |-  ( E. y e. B ph <-> -. A. y e. B -. ph )
22 21 sbcbii 
 |-  ( [. A / x ]. E. y e. B ph <-> [. A / x ]. -. A. y e. B -. ph )
23 dfrex2 
 |-  ( E. y e. B [. A / x ]. ph <-> -. A. y e. B -. [. A / x ]. ph )
24 20 22 23 3bitr4g 
 |-  ( ( F/_ y A /\ A e. _V ) -> ( [. A / x ]. E. y e. B ph <-> E. y e. B [. A / x ]. ph ) )
25 24 ex 
 |-  ( F/_ y A -> ( A e. _V -> ( [. A / x ]. E. y e. B ph <-> E. y e. B [. A / x ]. ph ) ) )
26 2 9 25 pm5.21ndd 
 |-  ( F/_ y A -> ( [. A / x ]. E. y e. B ph <-> E. y e. B [. A / x ]. ph ) )