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