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

Metamath Proof Explorer

Theorem elabrex

Description: Elementhood in an image set. (Contributed by Mario Carneiro, 14-Jan-2014)

Ref Expression
Hypothesis elabrex.1 
|- B e. _V
Assertion elabrex 
|- ( x e. A -> B e. { y | E. x e. A y = B } )

Proof

Step Hyp Ref Expression
1 elabrex.1 
 |-  B e. _V
2 tru 
 |-  T.
3 csbeq1a 
 |-  ( x = z -> B = [_ z / x ]_ B )
4 3 equcoms 
 |-  ( z = x -> B = [_ z / x ]_ B )
5 trud 
 |-  ( z = x -> T. )
6 4 5 2thd 
 |-  ( z = x -> ( B = [_ z / x ]_ B <-> T. ) )
7 6 rspcev 
 |-  ( ( x e. A /\ T. ) -> E. z e. A B = [_ z / x ]_ B )
8 2 7 mpan2 
 |-  ( x e. A -> E. z e. A B = [_ z / x ]_ B )
9 eqeq1 
 |-  ( y = B -> ( y = [_ z / x ]_ B <-> B = [_ z / x ]_ B ) )
10 9 rexbidv 
 |-  ( y = B -> ( E. z e. A y = [_ z / x ]_ B <-> E. z e. A B = [_ z / x ]_ B ) )
11 1 10 elab 
 |-  ( B e. { y | E. z e. A y = [_ z / x ]_ B } <-> E. z e. A B = [_ z / x ]_ B )
12 8 11 sylibr 
 |-  ( x e. A -> B e. { y | E. z e. A y = [_ z / x ]_ B } )
13 nfv 
 |-  F/ z y = B
14 nfcsb1v 
 |-  F/_ x [_ z / x ]_ B
15 14 nfeq2 
 |-  F/ x y = [_ z / x ]_ B
16 3 eqeq2d 
 |-  ( x = z -> ( y = B <-> y = [_ z / x ]_ B ) )
17 13 15 16 cbvrexw 
 |-  ( E. x e. A y = B <-> E. z e. A y = [_ z / x ]_ B )
18 17 abbii 
 |-  { y | E. x e. A y = B } = { y | E. z e. A y = [_ z / x ]_ B }
19 12 18 eleqtrrdi 
 |-  ( x e. A -> B e. { y | E. x e. A y = B } )