Metamath Proof Explorer


Theorem elfv

Description: Membership in a function value. (Contributed by NM, 30-Apr-2004)

Ref Expression
Assertion elfv
|- ( A e. ( F ` B ) <-> E. x ( A e. x /\ A. y ( B F y <-> y = x ) ) )

Proof

Step Hyp Ref Expression
1 fv2
 |-  ( F ` B ) = U. { x | A. y ( B F y <-> y = x ) }
2 1 eleq2i
 |-  ( A e. ( F ` B ) <-> A e. U. { x | A. y ( B F y <-> y = x ) } )
3 eluniab
 |-  ( A e. U. { x | A. y ( B F y <-> y = x ) } <-> E. x ( A e. x /\ A. y ( B F y <-> y = x ) ) )
4 2 3 bitri
 |-  ( A e. ( F ` B ) <-> E. x ( A e. x /\ A. y ( B F y <-> y = x ) ) )