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