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  9603  cantnfp1lem3  9611  cantnflem1b  9617  cantnflem1  9620  cnfcom  9631  axdc3lem2  10382  inar1  10706  efgmnvl  19629  bnj967  34929  dford3  43011  limsuc2  43024  ordsssucim  43385  ordelordALT  44521  onfrALTlem2  44530  ordelordALTVD  44850  onfrALTlem2VD  44872  iunord  49659