This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eufsn

Description: There is exactly one function into a singleton, assuming ax-rep . See eufsn2 for different axiom requirements. If existence is not needed, use mofsn or mofsn2 for fewer axiom assumptions. (Contributed by Zhi Wang, 19-Sep-2024)

	Ref	Expression
Hypotheses	eufsn.1	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	eufsn.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
Assertion	eufsn	⊢ ( 𝜑 → ∃! 𝑓 𝑓 : 𝐴 ⟶ { 𝐵 } )

Proof

Step	Hyp	Ref	Expression
1		eufsn.1	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
2		eufsn.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		fconstmpt	⊢ ( 𝐴 × { 𝐵 } ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
4		mptexg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
5	3 4	eqeltrid	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 × { 𝐵 } ) ∈ V )
6	2 5	syl	⊢ ( 𝜑 → ( 𝐴 × { 𝐵 } ) ∈ V )
7	1 6	eufsnlem	⊢ ( 𝜑 → ∃! 𝑓 𝑓 : 𝐴 ⟶ { 𝐵 } )