Theorem ordtr 6375

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

Syntax hints:   → wi 4  Tr wtr 5220   E cep 5561   We wwe 5614  Ord word 6360

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 210  df-an 401  df-ord 6364

This theorem is referenced by:  ordelss  6377  ordn2lp  6381  ordelord  6383  tz7.7  6387  ordelssne  6388  ordin  6392  ordtr1  6406  orduniss  6461  ontr  6473  dford5  7783  ordsuci  7807  ordunisuc  7828  limsuc  7845  trom  7871  dfrecs3  8359  tz7.44-2  8394  cantnflt  9641  cantnfp1lem3  9649  cantnflem1b  9655  cantnflem1  9658  cnfcom  9669  axdc3lem2  10435  inar1  10760  efgmnvl  19784  bnj967  35278  dford3  43682  limsuc2  43695  ordsssucim  44056  ordelordALT  45173  onfrALTlem2  45182  ordelordALTVD  45502  onfrALTlem2VD  45524  iunord  50374