Theorem eufsn

Description: There is exactly one function into a singleton, assuming ax-rep . See eufsn2 for different axiom requirements. If existence is not needed, use mofsn or mofsn2 for fewer axiom assumptions. (Contributed by Zhi Wang, 19-Sep-2024)

	Ref	Expression
Hypotheses	eufsn.1	$$⊢\phi \to B\in W$$
	eufsn.2	$$⊢\phi \to A\in V$$
Assertion	eufsn	$$⊢\phi \to \exists !ff:A⟶\left\{B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		eufsn.1	$$⊢\phi \to B\in W$$
2		eufsn.2	$$⊢\phi \to A\in V$$
3		fconstmpt	$$⊢A\times \left\{B\right\}=\left(x\in A⟼B\right)$$
4		mptexg	$$⊢A\in V\to \left(x\in A⟼B\right)\in \mathrm{V}$$
5	3 4	eqeltrid	$$⊢A\in V\to A\times \left\{B\right\}\in \mathrm{V}$$
6	2 5	syl	$$⊢\phi \to A\times \left\{B\right\}\in \mathrm{V}$$
7	1 6	eufsnlem	$$⊢\phi \to \exists !ff:A⟶\left\{B\right\}$$