Metamath Proof Explorer

Theorem eluniima

Description: Membership in the union of an image of a function. (Contributed by NM, 28-Sep-2006)

Ref Expression
Assertion eluniima 
|- ( Fun F -> ( B e. U. ( F " A ) <-> E. x e. A B e. ( F ` x ) ) )

Proof

Step Hyp Ref Expression
1 funiunfv 
 |-  ( Fun F -> U_ x e. A ( F ` x ) = U. ( F " A ) )
2 1 eleq2d 
 |-  ( Fun F -> ( B e. U_ x e. A ( F ` x ) <-> B e. U. ( F " A ) ) )
3 eliun 
 |-  ( B e. U_ x e. A ( F ` x ) <-> E. x e. A B e. ( F ` x ) )
4 2 3 bitr3di 
 |-  ( Fun F -> ( B e. U. ( F " A ) <-> E. x e. A B e. ( F ` x ) ) )