Metamath Proof Explorer


Theorem fsn2g

Description: A function that maps a singleton to a class is the singleton of an ordered pair. (Contributed by Thierry Arnoux, 11-Jul-2020)

Ref Expression
Assertion fsn2g AVF:ABFABF=AFA

Proof

Step Hyp Ref Expression
1 sneq a=Aa=A
2 1 feq2d a=AF:aBF:AB
3 fveq2 a=AFa=FA
4 3 eleq1d a=AFaBFAB
5 id a=Aa=A
6 5 3 opeq12d a=AaFa=AFA
7 6 sneqd a=AaFa=AFA
8 7 eqeq2d a=AF=aFaF=AFA
9 4 8 anbi12d a=AFaBF=aFaFABF=AFA
10 vex aV
11 10 fsn2 F:aBFaBF=aFa
12 2 9 11 vtoclbg AVF:ABFABF=AFA