Metamath Proof Explorer

Theorem mofmo

Description: There is at most one function into a class containing at most one element. (Contributed by Zhi Wang, 19-Sep-2024)

Ref Expression
Assertion mofmo 
|- ( E* x x e. B -> E* f f : A --> B )

Proof

Step Hyp Ref Expression
1 mo0sn 
 |-  ( E* x x e. B <-> ( B = (/) \/ E. y B = { y } ) )
2 mof02 
 |-  ( B = (/) -> E* f f : A --> B )
3 mofsn2 
 |-  ( B = { y } -> E* f f : A --> B )
4 3 exlimiv 
 |-  ( E. y B = { y } -> E* f f : A --> B )
5 2 4 jaoi 
 |-  ( ( B = (/) \/ E. y B = { y } ) -> E* f f : A --> B )
6 1 5 sylbi 
 |-  ( E* x x e. B -> E* f f : A --> B )