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