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 } )