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

Metamath Proof Explorer

Theorem bnj89

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypothesis bnj89.1 
|- Z e. _V
Assertion bnj89 
|- ( [. Z / y ]. E! x ph <-> E! x [. Z / y ]. ph )

Proof

Step Hyp Ref Expression
1 bnj89.1 
 |-  Z e. _V
2 sbcex2 
 |-  ( [. Z / y ]. E. w A. x ( ph <-> x = w ) <-> E. w [. Z / y ]. A. x ( ph <-> x = w ) )
3 sbcal 
 |-  ( [. Z / y ]. A. x ( ph <-> x = w ) <-> A. x [. Z / y ]. ( ph <-> x = w ) )
4 3 exbii 
 |-  ( E. w [. Z / y ]. A. x ( ph <-> x = w ) <-> E. w A. x [. Z / y ]. ( ph <-> x = w ) )
5 sbcbig 
 |-  ( Z e. _V -> ( [. Z / y ]. ( ph <-> x = w ) <-> ( [. Z / y ]. ph <-> [. Z / y ]. x = w ) ) )
6 1 5 ax-mp 
 |-  ( [. Z / y ]. ( ph <-> x = w ) <-> ( [. Z / y ]. ph <-> [. Z / y ]. x = w ) )
7 sbcg 
 |-  ( Z e. _V -> ( [. Z / y ]. x = w <-> x = w ) )
8 1 7 ax-mp 
 |-  ( [. Z / y ]. x = w <-> x = w )
9 8 bibi2i 
 |-  ( ( [. Z / y ]. ph <-> [. Z / y ]. x = w ) <-> ( [. Z / y ]. ph <-> x = w ) )
10 6 9 bitri 
 |-  ( [. Z / y ]. ( ph <-> x = w ) <-> ( [. Z / y ]. ph <-> x = w ) )
11 10 albii 
 |-  ( A. x [. Z / y ]. ( ph <-> x = w ) <-> A. x ( [. Z / y ]. ph <-> x = w ) )
12 11 exbii 
 |-  ( E. w A. x [. Z / y ]. ( ph <-> x = w ) <-> E. w A. x ( [. Z / y ]. ph <-> x = w ) )
13 2 4 12 3bitri 
 |-  ( [. Z / y ]. E. w A. x ( ph <-> x = w ) <-> E. w A. x ( [. Z / y ]. ph <-> x = w ) )
14 eu6 
 |-  ( E! x ph <-> E. w A. x ( ph <-> x = w ) )
15 14 sbcbii 
 |-  ( [. Z / y ]. E! x ph <-> [. Z / y ]. E. w A. x ( ph <-> x = w ) )
16 eu6 
 |-  ( E! x [. Z / y ]. ph <-> E. w A. x ( [. Z / y ]. ph <-> x = w ) )
17 13 15 16 3bitr4i 
 |-  ( [. Z / y ]. E! x ph <-> E! x [. Z / y ]. ph )