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 ( 𝐹 : 𝐴 ⟶ { 𝐵 } ↔ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ffnfv ⊢ ( 𝐹 : 𝐴 ⟶ { 𝐵 } ↔ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ { 𝐵 } ) )
2 fvex ⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
3 2 elsn ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ { 𝐵 } ↔ ( 𝐹 ‘ 𝑥 ) = 𝐵 )
4 3 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ { 𝐵 } ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝐵 )
5 4 anbi2i ⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ { 𝐵 } ) ↔ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝐵 ) )
6 1 5 bitri ⊢ ( 𝐹 : 𝐴 ⟶ { 𝐵 } ↔ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝐵 ) )