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