Theorem ordtr 6371

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

Syntax hints:   → wi 4  Tr wtr 5234   E cep 5557   We wwe 5610  Ord word 6356

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 6360

This theorem is referenced by:  ordelss  6373  ordn2lp  6377  ordelord  6379  tz7.7  6383  ordelssne  6384  ordin  6387  ordtr1  6401  orduniss  6456  ontr  6468  dford5  7783  ordsuci  7807  ordunisuc  7831  limsuc  7849  trom  7875  dfrecs3  8391  dfrecs3OLD  8392  tz7.44-2  8426  cantnflt  9691  cantnfp1lem3  9699  cantnflem1b  9705  cantnflem1  9708  cnfcom  9719  axdc3lem2  10470  inar1  10794  efgmnvl  19700  bnj967  34981  dford3  43019  limsuc2  43032  ordsssucim  43393  ordelordALT  44529  onfrALTlem2  44538  ordelordALTVD  44858  onfrALTlem2VD  44880  iunord  49507