Metamath Proof Explorer

Theorem mapdm0

Description: The empty set is the only map with empty domain. (Contributed by Glauco Siliprandi, 11-Oct-2020) (Proof shortened by Thierry Arnoux, 3-Dec-2021)

Ref Expression
Assertion mapdm0 ⊢ B ∈ V → B ∅ = ∅

Proof

Step Hyp Ref Expression
1 0ex ⊢ ∅ ∈ V
2 elmapg ⊢ B ∈ V ∧ ∅ ∈ V → f ∈ B ∅ ↔ f : ∅ ⟶ B
3 1 2 mpan2 ⊢ B ∈ V → f ∈ B ∅ ↔ f : ∅ ⟶ B
4 f0bi ⊢ f : ∅ ⟶ B ↔ f = ∅
5 3 4 bitrdi ⊢ B ∈ V → f ∈ B ∅ ↔ f = ∅
6 velsn ⊢ f ∈ ∅ ↔ f = ∅
7 5 6 bitr4di ⊢ B ∈ V → f ∈ B ∅ ↔ f ∈ ∅
8 7 eqrdv ⊢ B ∈ V → B ∅ = ∅