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

Metamath Proof Explorer

Theorem elabrexg

Description: Elementhood in an image set. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion elabrexg 
|- ( ( x e. A /\ B e. V ) -> B e. { y | E. x e. A y = B } )

Proof

Step Hyp Ref Expression
1 tru 
 |-  T.
2 csbeq1a 
 |-  ( x = z -> B = [_ z / x ]_ B )
3 2 equcoms 
 |-  ( z = x -> B = [_ z / x ]_ B )
4 trud 
 |-  ( z = x -> T. )
5 3 4 2thd 
 |-  ( z = x -> ( B = [_ z / x ]_ B <-> T. ) )
6 5 rspcev 
 |-  ( ( x e. A /\ T. ) -> E. z e. A B = [_ z / x ]_ B )
7 1 6 mpan2 
 |-  ( x e. A -> E. z e. A B = [_ z / x ]_ B )
8 7 adantr 
 |-  ( ( x e. A /\ B e. V ) -> 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 10 elabg 
 |-  ( B e. V -> ( B e. { y | E. z e. A y = [_ z / x ]_ B } <-> E. z e. A B = [_ z / x ]_ B ) )
12 11 adantl 
 |-  ( ( x e. A /\ B e. V ) -> ( B e. { y | E. z e. A y = [_ z / x ]_ B } <-> E. z e. A B = [_ z / x ]_ B ) )
13 8 12 mpbird 
 |-  ( ( x e. A /\ B e. V ) -> B e. { y | E. z e. A y = [_ z / x ]_ B } )
14 nfv 
 |-  F/ z y = B
15 nfcsb1v 
 |-  F/_ x [_ z / x ]_ B
16 15 nfeq2 
 |-  F/ x y = [_ z / x ]_ B
17 2 eqeq2d 
 |-  ( x = z -> ( y = B <-> y = [_ z / x ]_ B ) )
18 14 16 17 cbvrexw 
 |-  ( E. x e. A y = B <-> E. z e. A y = [_ z / x ]_ B )
19 18 abbii 
 |-  { y | E. x e. A y = B } = { y | E. z e. A y = [_ z / x ]_ B }
20 13 19 eleqtrrdi 
 |-  ( ( x e. A /\ B e. V ) -> B e. { y | E. x e. A y = B } )