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 (/) ) = { (/) } )