Theorem ordtr 6334

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

Syntax hints:   → wi 4  Tr wtr 5209   E cep 5530   We wwe 5583  Ord word 6319

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 6323

This theorem is referenced by:  ordelss  6336  ordn2lp  6340  ordelord  6342  tz7.7  6346  ordelssne  6347  ordin  6350  ordtr1  6364  orduniss  6419  ontr  6431  dford5  7740  ordsuci  7764  ordunisuc  7787  limsuc  7805  trom  7831  dfrecs3  8318  tz7.44-2  8352  cantnflt  9601  cantnfp1lem3  9609  cantnflem1b  9615  cantnflem1  9618  cnfcom  9629  axdc3lem2  10380  inar1  10704  efgmnvl  19628  bnj967  34928  dford3  43010  limsuc2  43023  ordsssucim  43384  ordelordALT  44520  onfrALTlem2  44529  ordelordALTVD  44849  onfrALTlem2VD  44871  iunord  49658