Theorem ordtr 6333

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 6322	. 2 ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
2	1	simplbi 496	1 ⊢ (Ord 𝐴 → Tr 𝐴)

Syntax hints:   → wi 4  Tr wtr 5193   E cep 5525   We wwe 5578  Ord word 6318

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 6322

This theorem is referenced by:  ordelss  6335  ordn2lp  6339  ordelord  6341  tz7.7  6345  ordelssne  6346  ordin  6349  ordtr1  6363  orduniss  6418  ontr  6430  dford5  7733  ordsuci  7757  ordunisuc  7778  limsuc  7795  trom  7821  dfrecs3  8307  tz7.44-2  8341  cantnflt  9588  cantnfp1lem3  9596  cantnflem1b  9602  cantnflem1  9605  cnfcom  9616  axdc3lem2  10368  inar1  10693  efgmnvl  19684  bnj967  35107  dford3  43480  limsuc2  43493  ordsssucim  43854  ordelordALT  44988  onfrALTlem2  44997  ordelordALTVD  45317  onfrALTlem2VD  45339  iunord  50169