Description: The domain of TopOn is the universal class _V . (Contributed by BJ, 29-Apr-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | dmtopon | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vpwex | |
|
2 | 1 | pwex | |
3 | eqcom | |
|
4 | 3 | rabbii | |
5 | rabssab | |
|
6 | pwpwssunieq | |
|
7 | 5 6 | sstri | |
8 | 4 7 | eqsstri | |
9 | 2 8 | ssexi | |
10 | df-topon | |
|
11 | 9 10 | dmmpti | |