Theorem fsetabsnop

Description: The class of all functions from a (proper) singleton into B is the class of all the singletons of (proper) ordered pairs over the elements of B as second component. (Contributed by AV, 13-Sep-2024)

	Ref	Expression
Assertion	fsetabsnop	$$⊢S\in V\to \left\{f|f:\left\{S\right\}⟶B\right\}=\left\{y|\exists b\in By=\left\{⟨S,b⟩\right\}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		fsetsniunop	$$⊢S\in V\to \left\{f|f:\left\{S\right\}⟶B\right\}=\bigcup _{b\in B}\left\{\left\{⟨S,b⟩\right\}\right\}$$
2		iunsn	$$⊢\bigcup _{b\in B}\left\{\left\{⟨S,b⟩\right\}\right\}=\left\{y|\exists b\in By=\left\{⟨S,b⟩\right\}\right\}$$
3	1 2	eqtrdi	$$⊢S\in V\to \left\{f|f:\left\{S\right\}⟶B\right\}=\left\{y|\exists b\in By=\left\{⟨S,b⟩\right\}\right\}$$