Theorem f10d

Description: The empty set maps one-to-one into any class, deduction version. (Contributed by AV, 25-Nov-2020)

	Ref	Expression
Hypothesis	f10d.f	$$⊢\phi \to F=\varnothing$$
Assertion	f10d	$$⊢\phi \to F:\mathrm{dom}F\underset{1-1}{⟶}A$$

Proof

Step	Hyp	Ref	Expression
1		f10d.f	$$⊢\phi \to F=\varnothing$$
2		f10	$$⊢\varnothing :\varnothing \underset{1-1}{⟶}A$$
3		dm0	$$⊢\mathrm{dom}\varnothing =\varnothing$$
4		f1eq2	$$⊢\mathrm{dom}\varnothing =\varnothing \to \left(\varnothing :\mathrm{dom}\varnothing \underset{1-1}{⟶}A\leftrightarrow \varnothing :\varnothing \underset{1-1}{⟶}A\right)$$
5	3 4	ax-mp	$$⊢\varnothing :\mathrm{dom}\varnothing \underset{1-1}{⟶}A\leftrightarrow \varnothing :\varnothing \underset{1-1}{⟶}A$$
6	2 5	mpbir	$$⊢\varnothing :\mathrm{dom}\varnothing \underset{1-1}{⟶}A$$
7	1	dmeqd	$$⊢\phi \to \mathrm{dom}F=\mathrm{dom}\varnothing$$
8		eqidd	$$⊢\phi \to A=A$$
9	1 7 8	f1eq123d	$$⊢\phi \to \left(F:\mathrm{dom}F\underset{1-1}{⟶}A\leftrightarrow \varnothing :\mathrm{dom}\varnothing \underset{1-1}{⟶}A\right)$$
10	6 9	mpbiri	$$⊢\phi \to F:\mathrm{dom}F\underset{1-1}{⟶}A$$