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

Proof

Step	Hyp	Ref	Expression
1		eufsn.1	|- ( ph -> B e. W )
2		eufsnlem.2	|- ( ph -> ( A X. { B } ) e. V )
3		fconst2g	|- ( B e. W -> ( f : A --> { B } <-> f = ( A X. { B } ) ) )
4	1 3	syl	|- ( ph -> ( f : A --> { B } <-> f = ( A X. { B } ) ) )
5	4	alrimiv	|- ( ph -> A. f ( f : A --> { B } <-> f = ( A X. { B } ) ) )
6		eqeq2	|- ( g = ( A X. { B } ) -> ( f = g <-> f = ( A X. { B } ) ) )
7	6	bibi2d	|- ( g = ( A X. { B } ) -> ( ( f : A --> { B } <-> f = g ) <-> ( f : A --> { B } <-> f = ( A X. { B } ) ) ) )
8	7	albidv	|- ( g = ( A X. { B } ) -> ( A. f ( f : A --> { B } <-> f = g ) <-> A. f ( f : A --> { B } <-> f = ( A X. { B } ) ) ) )
9	2 5 8	spcedv	|- ( ph -> E. g A. f ( f : A --> { B } <-> f = g ) )
10		eu6im	|- ( E. g A. f ( f : A --> { B } <-> f = g ) -> E! f f : A --> { B } )
11	9 10	syl	|- ( ph -> E! f f : A --> { B } )