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