This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fconstfv

Description: A constant function expressed in terms of its functionality, domain, and value. See also fconst2 . (Contributed by NM, 27-Aug-2004) (Proof shortened by OpenAI, 25-Mar-2020)

Ref Expression
Assertion fconstfv 
|- ( F : A --> { B } <-> ( F Fn A /\ A. x e. A ( F ` x ) = B ) )

Proof

Step Hyp Ref Expression
1 ffnfv 
 |-  ( F : A --> { B } <-> ( F Fn A /\ A. x e. A ( F ` x ) e. { B } ) )
2 fvex 
 |-  ( F ` x ) e. _V
3 2 elsn 
 |-  ( ( F ` x ) e. { B } <-> ( F ` x ) = B )
4 3 ralbii 
 |-  ( A. x e. A ( F ` x ) e. { B } <-> A. x e. A ( F ` x ) = B )
5 4 anbi2i 
 |-  ( ( F Fn A /\ A. x e. A ( F ` x ) e. { B } ) <-> ( F Fn A /\ A. x e. A ( F ` x ) = B ) )
6 1 5 bitri 
 |-  ( F : A --> { B } <-> ( F Fn A /\ A. x e. A ( F ` x ) = B ) )