Theorem ordtr 6341

Description: An ordinal class is transitive. (Contributed by NM, 3-Apr-1994.)

Assertion

Ref	Expression
ordtr	⊢ (Ord 𝐴 → Tr 𝐴)

Proof of Theorem ordtr

Step	Hyp	Ref	Expression
1		df-ord 6330	. 2 ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
2	1	simplbi 496	1 ⊢ (Ord 𝐴 → Tr 𝐴)

Syntax hints:   → wi 4  Tr wtr 5207   E cep 5533   We wwe 5586  Ord word 6326

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-ord 6330

This theorem is referenced by:  ordelss  6343  ordn2lp  6347  ordelord  6349  tz7.7  6353  ordelssne  6354  ordin  6357  ordtr1  6371  orduniss  6426  ontr  6438  dford5  7741  ordsuci  7765  ordunisuc  7786  limsuc  7803  trom  7829  dfrecs3  8316  tz7.44-2  8350  cantnflt  9595  cantnfp1lem3  9603  cantnflem1b  9609  cantnflem1  9612  cnfcom  9623  axdc3lem2  10375  inar1  10700  efgmnvl  19660  bnj967  35127  dford3  43414  limsuc2  43427  ordsssucim  43788  ordelordALT  44922  onfrALTlem2  44931  ordelordALTVD  45251  onfrALTlem2VD  45273  iunord  50064