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

Metamath Proof Explorer

Theorem mofsssn

Description: There is at most one function into a subclass of a singleton. (Contributed by Zhi Wang, 24-Sep-2024)

		Ref	Expression
	Assertion	mofsssn	$⊢ B \subseteq \{Y\} \to \exists^{*} f f : A ⟶ B$

Step	Hyp	Ref	Expression
1		sssn	$⊢ B \subseteq \{Y\} \leftrightarrow (B = \emptyset \lor B = \{Y\})$
2		mof02	$⊢ B = \emptyset \to \exists^{*} f f : A ⟶ B$
3		mofsn2	$⊢ B = \{Y\} \to \exists^{*} f f : A ⟶ B$
4	2 3	jaoi	$⊢ (B = \emptyset \lor B = \{Y\}) \to \exists^{*} f f : A ⟶ B$
5	1 4	sylbi	$⊢ B \subseteq \{Y\} \to \exists^{*} f f : A ⟶ B$