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	$$⊢\left\{f|f:\varnothing ⟶B\right\}=\left\{\varnothing \right\}$$

Proof

Step	Hyp	Ref	Expression
1		f0bi	$$⊢f:\varnothing ⟶B\leftrightarrow f=\varnothing$$
2	1	abbii	$$⊢\left\{f|f:\varnothing ⟶B\right\}=\left\{f|f=\varnothing \right\}$$
3		df-sn	$$⊢\left\{\varnothing \right\}=\left\{f|f=\varnothing \right\}$$
4	2 3	eqtr4i	$$⊢\left\{f|f:\varnothing ⟶B\right\}=\left\{\varnothing \right\}$$