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

Metamath Proof Explorer

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 } )