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	$⊢ φ \to B \in W$
	eufsn.2	$⊢ φ \to A \in V$
Assertion	eufsn	$⊢ φ \to \exists! f f : A ⟶ \{B\}$

Proof

Step	Hyp	Ref	Expression
1		eufsn.1	$⊢ φ \to B \in W$
2		eufsn.2	$⊢ φ \to A \in V$
3		fconstmpt	$⊢ A \times \{B\} = (x \in A ⟼ B)$
4		mptexg	$⊢ A \in V \to (x \in A ⟼ B) \in V$
5	3 4	eqeltrid	$⊢ A \in V \to A \times \{B\} \in V$
6	2 5	syl	$⊢ φ \to A \times \{B\} \in V$
7	1 6	eufsnlem	$⊢ φ \to \exists! f f : A ⟶ \{B\}$