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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sneq | |
|
2 | 1 | feq2d | |
3 | fveq2 | |
|
4 | 3 | eleq1d | |
5 | id | |
|
6 | 5 3 | opeq12d | |
7 | 6 | sneqd | |
8 | 7 | eqeq2d | |
9 | 4 8 | anbi12d | |
10 | vex | |
|
11 | 10 | fsn2 | |
12 | 2 9 11 | vtoclbg | |