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