Theorem f0dom0

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

	Ref	Expression
Assertion	f0dom0	⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → ( 𝑋 = ∅ ↔ 𝐹 = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		feq2	⊢ ( 𝑋 = ∅ → ( 𝐹 : 𝑋 ⟶ 𝑌 ↔ 𝐹 : ∅ ⟶ 𝑌 ) )
2		f0bi	⊢ ( 𝐹 : ∅ ⟶ 𝑌 ↔ 𝐹 = ∅ )
3	2	biimpi	⊢ ( 𝐹 : ∅ ⟶ 𝑌 → 𝐹 = ∅ )
4	1 3	biimtrdi	⊢ ( 𝑋 = ∅ → ( 𝐹 : 𝑋 ⟶ 𝑌 → 𝐹 = ∅ ) )
5	4	com12	⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → ( 𝑋 = ∅ → 𝐹 = ∅ ) )
6		feq1	⊢ ( 𝐹 = ∅ → ( 𝐹 : 𝑋 ⟶ 𝑌 ↔ ∅ : 𝑋 ⟶ 𝑌 ) )
7		fdm	⊢ ( ∅ : 𝑋 ⟶ 𝑌 → dom ∅ = 𝑋 )
8		dm0	⊢ dom ∅ = ∅
9	7 8	eqtr3di	⊢ ( ∅ : 𝑋 ⟶ 𝑌 → 𝑋 = ∅ )
10	6 9	biimtrdi	⊢ ( 𝐹 = ∅ → ( 𝐹 : 𝑋 ⟶ 𝑌 → 𝑋 = ∅ ) )
11	10	com12	⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → ( 𝐹 = ∅ → 𝑋 = ∅ ) )
12	5 11	impbid	⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → ( 𝑋 = ∅ ↔ 𝐹 = ∅ ) )