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 ( 𝐵𝑉 → ( 𝐵m ∅ ) = { ∅ } )

Proof

Step Hyp Ref Expression
1 0ex ∅ ∈ V
2 elmapg ( ( 𝐵𝑉 ∧ ∅ ∈ V ) → ( 𝑓 ∈ ( 𝐵m ∅ ) ↔ 𝑓 : ∅ ⟶ 𝐵 ) )
3 1 2 mpan2 ( 𝐵𝑉 → ( 𝑓 ∈ ( 𝐵m ∅ ) ↔ 𝑓 : ∅ ⟶ 𝐵 ) )
4 f0bi ( 𝑓 : ∅ ⟶ 𝐵𝑓 = ∅ )
5 3 4 bitrdi ( 𝐵𝑉 → ( 𝑓 ∈ ( 𝐵m ∅ ) ↔ 𝑓 = ∅ ) )
6 velsn ( 𝑓 ∈ { ∅ } ↔ 𝑓 = ∅ )
7 5 6 bitr4di ( 𝐵𝑉 → ( 𝑓 ∈ ( 𝐵m ∅ ) ↔ 𝑓 ∈ { ∅ } ) )
8 7 eqrdv ( 𝐵𝑉 → ( 𝐵m ∅ ) = { ∅ } )