Theorem f102g

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

	Ref	Expression
Assertion	f102g	|- ( ( A = (/) /\ F : A --> B ) -> F : A -1-1-> B )

Proof

Step	Hyp	Ref	Expression
1		feq2	|- ( A = (/) -> ( F : A --> B <-> F : (/) --> B ) )
2	1	biimpa	|- ( ( A = (/) /\ F : A --> B ) -> F : (/) --> B )
3		f0bi	|- ( F : (/) --> B <-> F = (/) )
4		f10	|- (/) : (/) -1-1-> B
5		f1eq1	|- ( F = (/) -> ( F : (/) -1-1-> B <-> (/) : (/) -1-1-> B ) )
6	4 5	mpbiri	|- ( F = (/) -> F : (/) -1-1-> B )
7	3 6	sylbi	|- ( F : (/) --> B -> F : (/) -1-1-> B )
8	2 7	syl	|- ( ( A = (/) /\ F : A --> B ) -> F : (/) -1-1-> B )
9		f1eq2	|- ( A = (/) -> ( F : A -1-1-> B <-> F : (/) -1-1-> B ) )
10	9	adantr	|- ( ( A = (/) /\ F : A --> B ) -> ( F : A -1-1-> B <-> F : (/) -1-1-> B ) )
11	8 10	mpbird	|- ( ( A = (/) /\ F : A --> B ) -> F : A -1-1-> B )