Metamath Proof Explorer


Theorem tsken

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 TTarskiATATAT

Proof

Step Hyp Ref Expression
1 eltskg TTarskiTTarskixT𝒫xTyT𝒫xyx𝒫TxTxT
2 1 ibi TTarskixT𝒫xTyT𝒫xyx𝒫TxTxT
3 2 simprd TTarskix𝒫TxTxT
4 elpw2g TTarskiA𝒫TAT
5 4 biimpar TTarskiATA𝒫T
6 breq1 x=AxTAT
7 eleq1 x=AxTAT
8 6 7 orbi12d x=AxTxTATAT
9 8 rspccva x𝒫TxTxTA𝒫TATAT
10 3 5 9 syl2an2r TTarskiATATAT