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 e. V -> ( B ^m (/) ) = { (/) } )

Proof

Step Hyp Ref Expression
1 0ex
 |-  (/) e. _V
2 elmapg
 |-  ( ( B e. V /\ (/) e. _V ) -> ( f e. ( B ^m (/) ) <-> f : (/) --> B ) )
3 1 2 mpan2
 |-  ( B e. V -> ( f e. ( B ^m (/) ) <-> f : (/) --> B ) )
4 f0bi
 |-  ( f : (/) --> B <-> f = (/) )
5 3 4 bitrdi
 |-  ( B e. V -> ( f e. ( B ^m (/) ) <-> f = (/) ) )
6 velsn
 |-  ( f e. { (/) } <-> f = (/) )
7 5 6 bitr4di
 |-  ( B e. V -> ( f e. ( B ^m (/) ) <-> f e. { (/) } ) )
8 7 eqrdv
 |-  ( B e. V -> ( B ^m (/) ) = { (/) } )