Theorem f1o0

Description: One-to-one onto mapping of the empty set. (Contributed by NM, 10-Sep-2004)

	Ref	Expression
Assertion	f1o0	$$⊢\varnothing :\varnothing \underset{1-1\; onto}{⟶}\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\varnothing =\varnothing$$
2		f1o00	$$⊢\varnothing :\varnothing \underset{1-1\; onto}{⟶}\varnothing \leftrightarrow \left(\varnothing =\varnothing \wedge \varnothing =\varnothing \right)$$
3	1 1 2	mpbir2an	$$⊢\varnothing :\varnothing \underset{1-1\; onto}{⟶}\varnothing$$