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 \left\{Y\right\}\to {\exists }^{*}ff:A⟶B$$

Proof

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