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

Metamath Proof Explorer

Theorem f1sn2g

Description: A function that maps a singleton to a class is injective. (Contributed by Zhi Wang, 1-Oct-2024)

Ref Expression
Assertion f1sn2g 
|- ( ( A e. V /\ F : { A } --> B ) -> F : { A } -1-1-> B )

Proof

Step Hyp Ref Expression
1 fsn2g 
 |-  ( A e. V -> ( F : { A } --> B <-> ( ( F ` A ) e. B /\ F = { <. A , ( F ` A ) >. } ) ) )
2 1 biimpa 
 |-  ( ( A e. V /\ F : { A } --> B ) -> ( ( F ` A ) e. B /\ F = { <. A , ( F ` A ) >. } ) )
3 2 simpld 
 |-  ( ( A e. V /\ F : { A } --> B ) -> ( F ` A ) e. B )
4 f1sng 
 |-  ( ( A e. V /\ ( F ` A ) e. B ) -> { <. A , ( F ` A ) >. } : { A } -1-1-> B )
5 3 4 syldan 
 |-  ( ( A e. V /\ F : { A } --> B ) -> { <. A , ( F ` A ) >. } : { A } -1-1-> B )
6 f1eq1 
 |-  ( F = { <. A , ( F ` A ) >. } -> ( F : { A } -1-1-> B <-> { <. A , ( F ` A ) >. } : { A } -1-1-> B ) )
7 2 6 simpl2im 
 |-  ( ( A e. V /\ F : { A } --> B ) -> ( F : { A } -1-1-> B <-> { <. A , ( F ` A ) >. } : { A } -1-1-> B ) )
8 5 7 mpbird 
 |-  ( ( A e. V /\ F : { A } --> B ) -> F : { A } -1-1-> B )