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	$$⊢\phi \to B\in W$$
	eufsnlem.2	$$⊢\phi \to A\times \left\{B\right\}\in V$$
Assertion	eufsnlem	$$⊢\phi \to \exists !ff:A⟶\left\{B\right\}$$

Proof

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