Theorem f0bi

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

	Ref	Expression
Assertion	f0bi	⊢ ( 𝐹 : ∅ ⟶ 𝑋 ↔ 𝐹 = ∅ )

Proof

Step	Hyp	Ref	Expression
1		ffn	⊢ ( 𝐹 : ∅ ⟶ 𝑋 → 𝐹 Fn ∅ )
2		fn0	⊢ ( 𝐹 Fn ∅ ↔ 𝐹 = ∅ )
3	1 2	sylib	⊢ ( 𝐹 : ∅ ⟶ 𝑋 → 𝐹 = ∅ )
4		f0	⊢ ∅ : ∅ ⟶ 𝑋
5		feq1	⊢ ( 𝐹 = ∅ → ( 𝐹 : ∅ ⟶ 𝑋 ↔ ∅ : ∅ ⟶ 𝑋 ) )
6	4 5	mpbiri	⊢ ( 𝐹 = ∅ → 𝐹 : ∅ ⟶ 𝑋 )
7	3 6	impbii	⊢ ( 𝐹 : ∅ ⟶ 𝑋 ↔ 𝐹 = ∅ )