Theorem f0bi

Description: A function with empty domain is empty. (Contributed by Alexander van der Vekens, 30-Jun-2018)

	Ref	Expression
Assertion	f0bi	$$⊢F:\varnothing ⟶X\leftrightarrow F=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		ffn	$$⊢F:\varnothing ⟶X\to FFn\varnothing$$
2		fn0	$$⊢FFn\varnothing \leftrightarrow F=\varnothing$$
3	1 2	sylib	$$⊢F:\varnothing ⟶X\to F=\varnothing$$
4		f0	$$⊢\varnothing :\varnothing ⟶X$$
5		feq1	$$⊢F=\varnothing \to \left(F:\varnothing ⟶X\leftrightarrow \varnothing :\varnothing ⟶X\right)$$
6	4 5	mpbiri	$$⊢F=\varnothing \to F:\varnothing ⟶X$$
7	3 6	impbii	$$⊢F:\varnothing ⟶X\leftrightarrow F=\varnothing$$