Theorem eufsn2

Description: There is exactly one function into a singleton, assuming ax-pow and ax-un . Variant of eufsn . 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	eufsn2	|- ( 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		snex	|- { B } e. _V
4		xpexg	|- ( ( A e. V /\ { B } e. _V ) -> ( A X. { B } ) e. _V )
5	2 3 4	sylancl	|- ( ph -> ( A X. { B } ) e. _V )
6	1 5	eufsnlem	|- ( ph -> E! f f : A --> { B } )