Metamath Proof Explorer

Theorem fconst3

Description: Two ways to express a constant function. (Contributed by NM, 15-Mar-2007)

Ref Expression
Assertion fconst3 
|- ( F : A --> { B } <-> ( F Fn A /\ A C_ ( `' F " { B } ) ) )

Proof

Step Hyp Ref Expression
1 fconstfv 
 |-  ( F : A --> { B } <-> ( F Fn A /\ A. x e. A ( F ` x ) = B ) )
2 fnfun 
 |-  ( F Fn A -> Fun F )
3 fndm 
 |-  ( F Fn A -> dom F = A )
4 eqimss2 
 |-  ( dom F = A -> A C_ dom F )
5 3 4 syl 
 |-  ( F Fn A -> A C_ dom F )
6 funconstss 
 |-  ( ( Fun F /\ A C_ dom F ) -> ( A. x e. A ( F ` x ) = B <-> A C_ ( `' F " { B } ) ) )
7 2 5 6 syl2anc 
 |-  ( F Fn A -> ( A. x e. A ( F ` x ) = B <-> A C_ ( `' F " { B } ) ) )
8 7 pm5.32i 
 |-  ( ( F Fn A /\ A. x e. A ( F ` x ) = B ) <-> ( F Fn A /\ A C_ ( `' F " { B } ) ) )
9 1 8 bitri 
 |-  ( F : A --> { B } <-> ( F Fn A /\ A C_ ( `' F " { B } ) ) )