Metamath Proof Explorer


Theorem r1omtsk

Description: The set of hereditarily finite sets is a Tarski class. (The Tarski-Grothendieck Axiom is not needed for this theorem.) (Contributed by Mario Carneiro, 28-May-2013)

Ref Expression
Assertion r1omtsk R1ωTarski

Proof

Step Hyp Ref Expression
1 omina ωInacc
2 inatsk ωInaccR1ωTarski
3 1 2 ax-mp R1ωTarski