Theorem mofsn2

Description: There is at most one function into a singleton. An unconditional variant of mofsn , i.e., the singleton could be empty if Y is a proper class. (Contributed by Zhi Wang, 19-Sep-2024)

	Ref	Expression
Assertion	mofsn2	|- ( B = { Y } -> E* f f : A --> B )

Proof

Step	Hyp	Ref	Expression
1		mofsn	|- ( Y e. _V -> E* f f : A --> { Y } )
2	1	adantl	|- ( ( B = { Y } /\ Y e. _V ) -> E* f f : A --> { Y } )
3		feq3	|- ( B = { Y } -> ( f : A --> B <-> f : A --> { Y } ) )
4	3	mobidv	|- ( B = { Y } -> ( E* f f : A --> B <-> E* f f : A --> { Y } ) )
5	4	adantr	|- ( ( B = { Y } /\ Y e. _V ) -> ( E* f f : A --> B <-> E* f f : A --> { Y } ) )
6	2 5	mpbird	|- ( ( B = { Y } /\ Y e. _V ) -> E* f f : A --> B )
7		simpl	|- ( ( B = { Y } /\ -. Y e. _V ) -> B = { Y } )
8		snprc	|- ( -. Y e. _V <-> { Y } = (/) )
9	8	biimpi	|- ( -. Y e. _V -> { Y } = (/) )
10	9	adantl	|- ( ( B = { Y } /\ -. Y e. _V ) -> { Y } = (/) )
11	7 10	eqtrd	|- ( ( B = { Y } /\ -. Y e. _V ) -> B = (/) )
12		mof02	|- ( B = (/) -> E* f f : A --> B )
13	11 12	syl	|- ( ( B = { Y } /\ -. Y e. _V ) -> E* f f : A --> B )
14	6 13	pm2.61dan	|- ( B = { Y } -> E* f f : A --> B )