Theorem mofmo

Description: There is at most one function into a class containing at most one element. (Contributed by Zhi Wang, 19-Sep-2024)

	Ref	Expression
Assertion	mofmo	$$⊢{\exists }^{*}xx\in B\to {\exists }^{*}ff:A⟶B$$

Proof

Step	Hyp	Ref	Expression
1		mo0sn	$$⊢{\exists }^{*}xx\in B\leftrightarrow \left(B=\varnothing \vee \exists yB=\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	3	exlimiv	$$⊢\exists yB=\left\{y\right\}\to {\exists }^{*}ff:A⟶B$$
5	2 4	jaoi	$$⊢\left(B=\varnothing \vee \exists yB=\left\{y\right\}\right)\to {\exists }^{*}ff:A⟶B$$
6	1 5	sylbi	$$⊢{\exists }^{*}xx\in B\to {\exists }^{*}ff:A⟶B$$