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 =