Metamath Proof Explorer

Theorem elima2

Description: Membership in an image. Theorem 34 of Suppes p. 65. (Contributed by NM, 11-Aug-2004)

Ref Expression
Hypothesis elima.1 
|- A e. _V
Assertion elima2 
|- ( A e. ( B " C ) <-> E. x ( x e. C /\ x B A ) )

Proof

Step Hyp Ref Expression
1 elima.1 
 |-  A e. _V
2 1 elima 
 |-  ( A e. ( B " C ) <-> E. x e. C x B A )
3 df-rex 
 |-  ( E. x e. C x B A <-> E. x ( x e. C /\ x B A ) )
4 2 3 bitri 
 |-  ( A e. ( B " C ) <-> E. x ( x e. C /\ x B A ) )