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 )