Metamath Proof Explorer


Theorem 0tsk

Description: The empty set is a (transitive) Tarski class. (Contributed by FL, 30-Dec-2010)

Ref Expression
Assertion 0tsk Tarski

Proof

Step Hyp Ref Expression
1 ral0 x𝒫x𝒫x
2 elsni xx=
3 0ex V
4 3 enref
5 breq1 x=x
6 4 5 mpbiri x=x
7 6 orcd x=xx
8 2 7 syl xxx
9 pw0 𝒫=
10 8 9 eleq2s x𝒫xx
11 10 rgen x𝒫xx
12 eltsk2g VTarskix𝒫x𝒫xx𝒫xx
13 3 12 ax-mp Tarskix𝒫x𝒫xx𝒫xx
14 1 11 13 mpbir2an Tarski