Theorem mofsn

Description: There is at most one function into a singleton, with fewer axioms than eufsn and eufsn2 . See also mofsn2 . (Contributed by Zhi Wang, 19-Sep-2024)

	Ref	Expression
Assertion	mofsn	|- ( B e. V -> E* f f : A --> { B } )

Proof

Step	Hyp	Ref	Expression
1		fconst2g	|- ( B e. V -> ( f : A --> { B } <-> f = ( A X. { B } ) ) )
2	1	biimpd	|- ( B e. V -> ( f : A --> { B } -> f = ( A X. { B } ) ) )
3		fconst2g	|- ( B e. V -> ( g : A --> { B } <-> g = ( A X. { B } ) ) )
4	3	biimpd	|- ( B e. V -> ( g : A --> { B } -> g = ( A X. { B } ) ) )
5		eqtr3	|- ( ( f = ( A X. { B } ) /\ g = ( A X. { B } ) ) -> f = g )
6	5	a1i	|- ( B e. V -> ( ( f = ( A X. { B } ) /\ g = ( A X. { B } ) ) -> f = g ) )
7	2 4 6	syl2and	|- ( B e. V -> ( ( f : A --> { B } /\ g : A --> { B } ) -> f = g ) )
8	7	alrimivv	|- ( B e. V -> A. f A. g ( ( f : A --> { B } /\ g : A --> { B } ) -> f = g ) )
9		feq1	|- ( f = g -> ( f : A --> { B } <-> g : A --> { B } ) )
10	9	mo4	|- ( E* f f : A --> { B } <-> A. f A. g ( ( f : A --> { B } /\ g : A --> { B } ) -> f = g ) )
11	8 10	sylibr	|- ( B e. V -> E* f f : A --> { B } )