Metamath Proof Explorer


Definition df-trans

Description: Define the class of all transitive sets. (Contributed by Scott Fenton, 31-Mar-2012)

Ref Expression
Assertion df-trans 𝖳𝗋𝖺𝗇𝗌 = V ran E E E

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctrans class 𝖳𝗋𝖺𝗇𝗌
1 cvv class V
2 cep class E
3 2 2 ccom class E E
4 3 2 cdif class E E E
5 4 crn class ran E E E
6 1 5 cdif class V ran E E E
7 0 6 wceq wff 𝖳𝗋𝖺𝗇𝗌 = V ran E E E