Theorem fset0

Description: The set of functions from the empty set is the singleton containing the empty set. (Contributed by AV, 13-Sep-2024)

	Ref	Expression
Assertion	fset0	⊢ { 𝑓 ∣ 𝑓 : ∅ ⟶ 𝐵 } = { ∅ }

Proof

Step	Hyp	Ref	Expression
1		f0bi	⊢ ( 𝑓 : ∅ ⟶ 𝐵 ↔ 𝑓 = ∅ )
2	1	abbii	⊢ { 𝑓 ∣ 𝑓 : ∅ ⟶ 𝐵 } = { 𝑓 ∣ 𝑓 = ∅ }
3		df-sn	⊢ { ∅ } = { 𝑓 ∣ 𝑓 = ∅ }
4	2 3	eqtr4i	⊢ { 𝑓 ∣ 𝑓 : ∅ ⟶ 𝐵 } = { ∅ }