Theorem ordtr 6379

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

Syntax hints:   → wi 4  Tr wtr 5266   E cep 5580   We wwe 5631  Ord word 6364

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 206  df-an 395  df-ord 6368

This theorem is referenced by:  ordelss  6381  ordn2lp  6385  ordelord  6387  tz7.7  6391  ordelssne  6392  ordin  6395  ordtr1  6408  orduniss  6462  ontr  6474  dford5  7775  ordsuci  7800  ordunisuc  7824  limsuc  7842  trom  7868  omsindsOLD  7881  dfrecs3  8376  dfrecs3OLD  8377  tz7.44-2  8411  cantnflt  9671  cantnfp1lem3  9679  cantnflem1b  9685  cantnflem1  9688  cnfcom  9699  axdc3lem2  10450  inar1  10774  efgmnvl  19625  bnj967  34252  dford3  42071  limsuc2  42087  ordsssucim  42457  ordelordALT  43602  onfrALTlem2  43611  ordelordALTVD  43932  onfrALTlem2VD  43954  iunord  47810