This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

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