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 V f | f : S B = y | b B y = S b

Proof

Step Hyp Ref Expression
1 fsetsniunop S V f | f : S B = b B S b
2 iunsn b B S b = y | b B y = S b
3 1 2 eqtrdi S V f | f : S B = y | b B y = S b