Metamath Proof Explorer


Theorem fniniseg

Description: Membership in the preimage of a singleton, under a function. (Contributed by Mario Carneiro, 12-May-2014) (Proof shortened by Mario Carneiro , 28-Apr-2015)

Ref Expression
Assertion fniniseg
|- ( F Fn A -> ( C e. ( `' F " { B } ) <-> ( C e. A /\ ( F ` C ) = B ) ) )

Proof

Step Hyp Ref Expression
1 elpreima
 |-  ( F Fn A -> ( C e. ( `' F " { B } ) <-> ( C e. A /\ ( F ` C ) e. { B } ) ) )
2 fvex
 |-  ( F ` C ) e. _V
3 2 elsn
 |-  ( ( F ` C ) e. { B } <-> ( F ` C ) = B )
4 3 anbi2i
 |-  ( ( C e. A /\ ( F ` C ) e. { B } ) <-> ( C e. A /\ ( F ` C ) = B ) )
5 1 4 bitrdi
 |-  ( F Fn A -> ( C e. ( `' F " { B } ) <-> ( C e. A /\ ( F ` C ) = B ) ) )