Theorem 0map0sn0

Description: The set of mappings of the empty set to the empty set is the singleton containing the empty set. (Contributed by AV, 31-Mar-2024)

	Ref	Expression
Assertion	0map0sn0	⊢ ( ∅ ↑m ∅ ) = { ∅ }

Proof

Step	Hyp	Ref	Expression
1		f0bi	⊢ ( 𝑓 : ∅ ⟶ ∅ ↔ 𝑓 = ∅ )
2	1	abbii	⊢ { 𝑓 ∣ 𝑓 : ∅ ⟶ ∅ } = { 𝑓 ∣ 𝑓 = ∅ }
3		0ex	⊢ ∅ ∈ V
4	3 3	mapval	⊢ ( ∅ ↑m ∅ ) = { 𝑓 ∣ 𝑓 : ∅ ⟶ ∅ }
5		df-sn	⊢ { ∅ } = { 𝑓 ∣ 𝑓 = ∅ }
6	2 4 5	3eqtr4i	⊢ ( ∅ ↑m ∅ ) = { ∅ }