Metamath Proof Explorer

Theorem elima

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

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

Proof

Step Hyp Ref Expression
1 elima.1 
 |-  A e. _V
2 elimag 
 |-  ( A e. _V -> ( A e. ( B " C ) <-> E. x e. C x B A ) )
3 1 2 ax-mp 
 |-  ( A e. ( B " C ) <-> E. x e. C x B A )