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 ∧ ∀ x ∈ A F ⁡ x = B

Proof

Step Hyp Ref Expression
1 ffnfv ⊢ F : A ⟶ B ↔ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B
2 fvex ⊢ F ⁡ x ∈ V
3 2 elsn ⊢ F ⁡ x ∈ B ↔ F ⁡ x = B
4 3 ralbii ⊢ ∀ x ∈ A F ⁡ x ∈ B ↔ ∀ x ∈ A F ⁡ x = B
5 4 anbi2i ⊢ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B ↔ F Fn A ∧ ∀ x ∈ A F ⁡ x = B
6 1 5 bitri ⊢ F : A ⟶ B ↔ F Fn A ∧ ∀ x ∈ A F ⁡ x = B