Theorem mofsn

Description: There is at most one function into a singleton, with fewer axioms than eufsn and eufsn2 . See also mofsn2 . (Contributed by Zhi Wang, 19-Sep-2024)

	Ref	Expression
Assertion	mofsn	$$⊢B\in V\to {\exists }^{*}ff:A⟶\left\{B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		fconst2g	$$⊢B\in V\to \left(f:A⟶\left\{B\right\}\leftrightarrow f=A\times \left\{B\right\}\right)$$
2	1	biimpd	$$⊢B\in V\to \left(f:A⟶\left\{B\right\}\to f=A\times \left\{B\right\}\right)$$
3		fconst2g	$$⊢B\in V\to \left(g:A⟶\left\{B\right\}\leftrightarrow g=A\times \left\{B\right\}\right)$$
4	3	biimpd	$$⊢B\in V\to \left(g:A⟶\left\{B\right\}\to g=A\times \left\{B\right\}\right)$$
5		eqtr3	$$⊢\left(f=A\times \left\{B\right\}\wedge g=A\times \left\{B\right\}\right)\to f=g$$
6	5	a1i	$$⊢B\in V\to \left(\left(f=A\times \left\{B\right\}\wedge g=A\times \left\{B\right\}\right)\to f=g\right)$$
7	2 4 6	syl2and	$$⊢B\in V\to \left(\left(f:A⟶\left\{B\right\}\wedge g:A⟶\left\{B\right\}\right)\to f=g\right)$$
8	7	alrimivv	$$⊢B\in V\to \forall f\forall g\left(\left(f:A⟶\left\{B\right\}\wedge g:A⟶\left\{B\right\}\right)\to f=g\right)$$
9		feq1	$$⊢f=g\to \left(f:A⟶\left\{B\right\}\leftrightarrow g:A⟶\left\{B\right\}\right)$$
10	9	mo4	$$⊢{\exists }^{*}ff:A⟶\left\{B\right\}\leftrightarrow \forall f\forall g\left(\left(f:A⟶\left\{B\right\}\wedge g:A⟶\left\{B\right\}\right)\to f=g\right)$$
11	8 10	sylibr	$$⊢B\in V\to {\exists }^{*}ff:A⟶\left\{B\right\}$$