Metamath Proof Explorer

Theorem mofsssn

Description: There is at most one function into a subclass of a singleton. (Contributed by Zhi Wang, 24-Sep-2024)

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

Proof

Step Hyp Ref Expression
1 sssn 
 |-  ( B C_ { Y } <-> ( B = (/) \/ B = { Y } ) )
2 mof02 
 |-  ( B = (/) -> E* f f : A --> B )
3 mofsn2 
 |-  ( B = { Y } -> E* f f : A --> B )
4 2 3 jaoi 
 |-  ( ( B = (/) \/ B = { Y } ) -> E* f f : A --> B )
5 1 4 sylbi 
 |-  ( B C_ { Y } -> E* f f : A --> B )