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

Metamath Proof Explorer

Theorem eufsnlem

Description: There is exactly one function into a singleton. For a simpler hypothesis, see eufsn assuming ax-rep , or eufsn2 assuming ax-pow and ax-un . (Contributed by Zhi Wang, 19-Sep-2024)

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

Proof

Step Hyp Ref Expression
1 eufsn.1 
 |-  ( ph -> B e. W )
2 eufsnlem.2 
 |-  ( ph -> ( A X. { B } ) e. V )
3 fconst2g 
 |-  ( B e. W -> ( f : A --> { B } <-> f = ( A X. { B } ) ) )
4 1 3 syl 
 |-  ( ph -> ( f : A --> { B } <-> f = ( A X. { B } ) ) )
5 4 alrimiv 
 |-  ( ph -> A. f ( f : A --> { B } <-> f = ( A X. { B } ) ) )
6 eqeq2 
 |-  ( g = ( A X. { B } ) -> ( f = g <-> f = ( A X. { B } ) ) )
7 6 bibi2d 
 |-  ( g = ( A X. { B } ) -> ( ( f : A --> { B } <-> f = g ) <-> ( f : A --> { B } <-> f = ( A X. { B } ) ) ) )
8 7 albidv 
 |-  ( g = ( A X. { B } ) -> ( A. f ( f : A --> { B } <-> f = g ) <-> A. f ( f : A --> { B } <-> f = ( A X. { B } ) ) ) )
9 2 5 8 spcedv 
 |-  ( ph -> E. g A. f ( f : A --> { B } <-> f = g ) )
10 eu6im 
 |-  ( E. g A. f ( f : A --> { B } <-> f = g ) -> E! f f : A --> { B } )
11 9 10 syl 
 |-  ( ph -> E! f f : A --> { B } )