Theorem ordtr 6337

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

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

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 6326

This theorem is referenced by:  ordelss  6339  ordn2lp  6343  ordelord  6345  tz7.7  6349  ordelssne  6350  ordin  6353  ordtr1  6367  orduniss  6422  ontr  6434  dford5  7738  ordsuci  7762  ordunisuc  7783  limsuc  7800  trom  7826  dfrecs3  8312  tz7.44-2  8346  cantnflt  9593  cantnfp1lem3  9601  cantnflem1b  9607  cantnflem1  9610  cnfcom  9621  axdc3lem2  10373  inar1  10698  efgmnvl  19689  bnj967  35087  dford3  43456  limsuc2  43469  ordsssucim  43830  ordelordALT  44964  onfrALTlem2  44973  ordelordALTVD  45293  onfrALTlem2VD  45315  iunord  50151