Theorem f10

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

	Ref	Expression
Assertion	f10	⊢ ∅ : ∅ –1-1→ 𝐴

Proof

Step	Hyp	Ref	Expression
1		f0	⊢ ∅ : ∅ ⟶ 𝐴
2		funcnv0	⊢ Fun ◡ ∅
3		df-f1	⊢ ( ∅ : ∅ –1-1→ 𝐴 ↔ ( ∅ : ∅ ⟶ 𝐴 ∧ Fun ◡ ∅ ) )
4	1 2 3	mpbir2an	⊢ ∅ : ∅ –1-1→ 𝐴