Theorem fconst2

Description: A constant function expressed as a Cartesian product. (Contributed by NM, 20-Aug-1999)

	Ref	Expression
Hypothesis	fvconst2.1	⊢ 𝐵 ∈ V
Assertion	fconst2	⊢ ( 𝐹 : 𝐴 ⟶ { 𝐵 } ↔ 𝐹 = ( 𝐴 × { 𝐵 } ) )

Proof

Step	Hyp	Ref	Expression
1		fvconst2.1	⊢ 𝐵 ∈ V
2		fconst2g	⊢ ( 𝐵 ∈ V → ( 𝐹 : 𝐴 ⟶ { 𝐵 } ↔ 𝐹 = ( 𝐴 × { 𝐵 } ) ) )
3	1 2	ax-mp	⊢ ( 𝐹 : 𝐴 ⟶ { 𝐵 } ↔ 𝐹 = ( 𝐴 × { 𝐵 } ) )