Metamath Proof Explorer


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 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 >. } } )