Theorem f10

Description: The empty set maps one-to-one into any class. (Contributed by NM, 7-Apr-1998)

	Ref	Expression
Assertion	f10	$$⊢\varnothing :\varnothing \underset{1-1}{⟶}A$$

Proof

Step	Hyp	Ref	Expression
1		f0	$$⊢\varnothing :\varnothing ⟶A$$
2		funcnv0	$$⊢\mathrm{Fun}{\varnothing }^{-1}$$
3		df-f1	$$⊢\varnothing :\varnothing \underset{1-1}{⟶}A\leftrightarrow \left(\varnothing :\varnothing ⟶A\wedge \mathrm{Fun}{\varnothing }^{-1}\right)$$
4	1 2 3	mpbir2an	$$⊢\varnothing :\varnothing \underset{1-1}{⟶}A$$