Theorem f002

Description: A function with an empty codomain must have empty domain. (Contributed by Zhi Wang, 1-Oct-2024)

	Ref	Expression
Hypothesis	f002.1	$$⊢\phi \to F:A⟶B$$
Assertion	f002	$$⊢\phi \to \left(B=\varnothing \to A=\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		f002.1	$$⊢\phi \to F:A⟶B$$
2		feq3	$$⊢B=\varnothing \to \left(F:A⟶B\leftrightarrow F:A⟶\varnothing \right)$$
3		f00	$$⊢F:A⟶\varnothing \leftrightarrow \left(F=\varnothing \wedge A=\varnothing \right)$$
4	3	simprbi	$$⊢F:A⟶\varnothing \to A=\varnothing$$
5	2 4	biimtrdi	$$⊢B=\varnothing \to \left(F:A⟶B\to A=\varnothing \right)$$
6	1 5	syl5com	$$⊢\phi \to \left(B=\varnothing \to A=\varnothing \right)$$