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

Metamath Proof Explorer

Theorem eufsn

Description: There is exactly one function into a singleton, assuming ax-rep . See eufsn2 for different axiom requirements. If existence is not needed, use mofsn or mofsn2 for fewer axiom assumptions. (Contributed by Zhi Wang, 19-Sep-2024)

Ref Expression
Hypotheses eufsn.1 
|- ( ph -> B e. W )
eufsn.2 
|- ( ph -> A e. V )
Assertion eufsn 
|- ( ph -> E! f f : A --> { B } )

Proof

Step Hyp Ref Expression
1 eufsn.1 
 |-  ( ph -> B e. W )
2 eufsn.2 
 |-  ( ph -> A e. V )
3 fconstmpt 
 |-  ( A X. { B } ) = ( x e. A |-> B )
4 mptexg 
 |-  ( A e. V -> ( x e. A |-> B ) e. _V )
5 3 4 eqeltrid 
 |-  ( A e. V -> ( A X. { B } ) e. _V )
6 2 5 syl 
 |-  ( ph -> ( A X. { B } ) e. _V )
7 1 6 eufsnlem 
 |-  ( ph -> E! f f : A --> { B } )