Description: The empty set is a (transitive) Tarski class. (Contributed by FL, 30-Dec-2010)
Ref | Expression | ||
---|---|---|---|
Assertion | 0tsk | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ral0 | |
|
2 | elsni | |
|
3 | 0ex | |
|
4 | 3 | enref | |
5 | breq1 | |
|
6 | 4 5 | mpbiri | |
7 | 6 | orcd | |
8 | 2 7 | syl | |
9 | pw0 | |
|
10 | 8 9 | eleq2s | |
11 | 10 | rgen | |
12 | eltsk2g | |
|
13 | 3 12 | ax-mp | |
14 | 1 11 13 | mpbir2an | |