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	|- ( ph -> B e. W )
	eufsn.2	|- ( ph -> A e. V )
Assertion	eufsn	|- ( ph -> E! f f : A --> { B } )

Proof

Step	Hyp	Ref	Expression
1		eufsn.1	|- ( ph -> B e. W )
2		eufsn.2	|- ( ph -> A e. V )
3		fconstmpt	|- ( A X. { B } ) = ( x e. A |-> B )
4		mptexg	|- ( A e. V -> ( x e. A |-> B ) e. _V )
5	3 4	eqeltrid	|- ( A e. V -> ( A X. { B } ) e. _V )
6	2 5	syl	|- ( ph -> ( A X. { B } ) e. _V )
7	1 6	eufsnlem	|- ( ph -> E! f f : A --> { B } )