This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sbcreu

Description: Interchange class substitution and restricted unique existential quantifier. (Contributed by NM, 24-Feb-2013) (Revised by NM, 18-Aug-2018)

Ref Expression
Assertion sbcreu 
|- ( [. 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 reurex 
 |-  ( E! y e. B [. A / x ]. ph -> E. y e. B [. A / x ]. ph )
3 sbcex 
 |-  ( [. A / x ]. ph -> A e. _V )
4 3 rexlimivw 
 |-  ( E. y e. B [. A / x ]. ph -> A e. _V )
5 2 4 syl 
 |-  ( E! y e. B [. A / x ]. ph -> A e. _V )
6 dfsbcq2 
 |-  ( z = A -> ( [ z / x ] E! y e. B ph <-> [. A / x ]. E! y e. B ph ) )
7 dfsbcq2 
 |-  ( z = A -> ( [ z / x ] ph <-> [. A / x ]. ph ) )
8 7 reubidv 
 |-  ( z = A -> ( E! y e. B [ z / x ] ph <-> E! y e. B [. A / x ]. ph ) )
9 nfcv 
 |-  F/_ x B
10 nfs1v 
 |-  F/ x [ z / x ] ph
11 9 10 nfreuw 
 |-  F/ x E! y e. B [ z / x ] ph
12 sbequ12 
 |-  ( x = z -> ( ph <-> [ z / x ] ph ) )
13 12 reubidv 
 |-  ( x = z -> ( E! y e. B ph <-> E! y e. B [ z / x ] ph ) )
14 11 13 sbiev 
 |-  ( [ z / x ] E! y e. B ph <-> E! y e. B [ z / x ] ph )
15 6 8 14 vtoclbg 
 |-  ( A e. _V -> ( [. A / x ]. E! y e. B ph <-> E! y e. B [. A / x ]. ph ) )
16 1 5 15 pm5.21nii 
 |-  ( [. A / x ]. E! y e. B ph <-> E! y e. B [. A / x ]. ph )