Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 dfsbcq2 
 |-  ( z = A -> ( [ z / x ] E. y e. B ph <-> [. A / x ]. E. y e. B ph ) )
2 dfsbcq2 
 |-  ( z = A -> ( [ z / x ] ph <-> [. A / x ]. ph ) )
3 2 rexbidv 
 |-  ( z = A -> ( E. y e. B [ z / x ] ph <-> E. y e. B [. A / x ]. ph ) )
4 nfcv 
 |-  F/_ x B
5 nfs1v 
 |-  F/ x [ z / x ] ph
6 4 5 nfrex 
 |-  F/ x E. y e. B [ z / x ] ph
7 sbequ12 
 |-  ( x = z -> ( ph <-> [ z / x ] ph ) )
8 7 rexbidv 
 |-  ( x = z -> ( E. y e. B ph <-> E. y e. B [ z / x ] ph ) )
9 6 8 sbie 
 |-  ( [ z / x ] E. y e. B ph <-> E. y e. B [ z / x ] ph )
10 1 3 9 vtoclbg 
 |-  ( A e. V -> ( [. A / x ]. E. y e. B ph <-> E. y e. B [. A / x ]. ph ) )