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

Metamath Proof Explorer

Theorem eufsnlem

Description: There is exactly one function into a singleton. For a simpler hypothesis, see eufsn assuming ax-rep , or eufsn2 assuming ax-pow and ax-un . (Contributed by Zhi Wang, 19-Sep-2024)

		Ref	Expression
	Hypotheses	eufsn.1	$⊢ φ \to B \in W$
		eufsnlem.2	$⊢ φ \to A \times \{B\} \in V$
	Assertion	eufsnlem	$⊢ φ \to \exists! f f : A ⟶ \{B\}$

Proof

Step	Hyp	Ref	Expression
1		eufsn.1	$⊢ φ \to B \in W$
2		eufsnlem.2	$⊢ φ \to A \times \{B\} \in V$
3		fconst2g	$⊢ B \in W \to (f : A ⟶ \{B\} \leftrightarrow f = A \times \{B\})$
4	1 3	syl	$⊢ φ \to (f : A ⟶ \{B\} \leftrightarrow f = A \times \{B\})$
5	4	alrimiv	$⊢ φ \to \forall f (f : A ⟶ \{B\} \leftrightarrow f = A \times \{B\})$
6		eqeq2	$⊢ g = A \times \{B\} \to (f = g \leftrightarrow f = A \times \{B\})$
7	6	bibi2d	$⊢ g = A \times \{B\} \to ((f : A ⟶ \{B\} \leftrightarrow f = g) \leftrightarrow (f : A ⟶ \{B\} \leftrightarrow f = A \times \{B\}))$
8	7	albidv	$⊢ g = A \times \{B\} \to (\forall f (f : A ⟶ \{B\} \leftrightarrow f = g) \leftrightarrow \forall f (f : A ⟶ \{B\} \leftrightarrow f = A \times \{B\}))$
9	2 5 8	spcedv	$⊢ φ \to \exists g \forall f (f : A ⟶ \{B\} \leftrightarrow f = g)$
10		eu6im	$⊢ \exists g \forall f (f : A ⟶ \{B\} \leftrightarrow f = g) \to \exists! f f : A ⟶ \{B\}$
11	9 10	syl	$⊢ φ \to \exists! f f : A ⟶ \{B\}$