Theorem f0dom0

Description: A function is empty iff it has an empty domain. (Contributed by AV, 10-Feb-2019)

	Ref	Expression
Assertion	f0dom0	$$⊢F:X⟶Y\to \left(X=\varnothing \leftrightarrow F=\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		feq2	$$⊢X=\varnothing \to \left(F:X⟶Y\leftrightarrow F:\varnothing ⟶Y\right)$$
2		f0bi	$$⊢F:\varnothing ⟶Y\leftrightarrow F=\varnothing$$
3	2	biimpi	$$⊢F:\varnothing ⟶Y\to F=\varnothing$$
4	1 3	biimtrdi	$$⊢X=\varnothing \to \left(F:X⟶Y\to F=\varnothing \right)$$
5	4	com12	$$⊢F:X⟶Y\to \left(X=\varnothing \to F=\varnothing \right)$$
6		feq1	$$⊢F=\varnothing \to \left(F:X⟶Y\leftrightarrow \varnothing :X⟶Y\right)$$
7		fdm	$$⊢\varnothing :X⟶Y\to \mathrm{dom}\varnothing =X$$
8		dm0	$$⊢\mathrm{dom}\varnothing =\varnothing$$
9	7 8	eqtr3di	$$⊢\varnothing :X⟶Y\to X=\varnothing$$
10	6 9	biimtrdi	$$⊢F=\varnothing \to \left(F:X⟶Y\to X=\varnothing \right)$$
11	10	com12	$$⊢F:X⟶Y\to \left(F=\varnothing \to X=\varnothing \right)$$
12	5 11	impbid	$$⊢F:X⟶Y\to \left(X=\varnothing \leftrightarrow F=\varnothing \right)$$