This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )