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