Description: Third axiom of a Tarski class. A subset of a Tarski class is either equipotent to the class or an element of the class. (Contributed by FL, 30-Dec-2010) (Revised by Mario Carneiro, 20-Sep-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | tsken | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eltskg | |
|
2 | 1 | ibi | |
3 | 2 | simprd | |
4 | elpw2g | |
|
5 | 4 | biimpar | |
6 | breq1 | |
|
7 | eleq1 | |
|
8 | 6 7 | orbi12d | |
9 | 8 | rspccva | |
10 | 3 5 9 | syl2an2r | |