Metamath Proof Explorer

Theorem fsetabsnop

Description: The class of all functions from a (proper) singleton into B is the set 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 e. V -> { f \| f : { S } --> B } = { y \| E. b e. B y = { <. S , b >. } } )

Proof

Step	Hyp	Ref	Expression
1		fsetsniunop	\|- ( S e. V -> { f \| f : { S } --> B } = U_ b e. B { { <. S , b >. } } )
2		iunsn	\|- U_ b e. B { { <. S , b >. } } = { y \| E. b e. B y = { <. S , b >. } }
3	1 2	eqtrdi	\|- ( S e. V -> { f \| f : { S } --> B } = { y \| E. b e. B y = { <. S , b >. } } )

Step

Hyp

Ref

Expression

fsetsniunop

 |-  ( S e. V -> { f | f : { S } --> B } = U_ b e. B { { <. S , b >. } } )

iunsn

 |-  U_ b e. B { { <. S , b >. } } = { y | E. b e. B y = { <. S , b >. } }

1 2

eqtrdi

 |-  ( S e. V -> { f | f : { S } --> B } = { y | E. b e. B y = { <. S , b >. } } )