Metamath Proof Explorer

Theorem elimag

Description: Membership in an image. Theorem 34 of Suppes p. 65. (Contributed by NM, 20-Jan-2007)

Ref Expression
Assertion elimag 
|- ( A e. V -> ( A e. ( B " C ) <-> E. x e. C x B A ) )

Proof

Step Hyp Ref Expression
1 breq2 
 |-  ( y = A -> ( x B y <-> x B A ) )
2 1 rexbidv 
 |-  ( y = A -> ( E. x e. C x B y <-> E. x e. C x B A ) )
3 dfima2 
 |-  ( B " C ) = { y | E. x e. C x B y }
4 2 3 elab2g 
 |-  ( A e. V -> ( A e. ( B " C ) <-> E. x e. C x B A ) )