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:ABFFnAxAFx=B

Proof

Step Hyp Ref Expression
1 ffnfv F:ABFFnAxAFxB
2 fvex FxV
3 2 elsn FxBFx=B
4 3 ralbii xAFxBxAFx=B
5 4 anbi2i FFnAxAFxBFFnAxAFx=B
6 1 5 bitri F:ABFFnAxAFx=B