This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝐹 : ∅ ⟶ 𝑋 ↔ 𝐹 = ∅ )