Theorem ordtr 6330

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

Syntax hints:   → wi 4  Tr wtr 5204   E cep 5522   We wwe 5575  Ord word 6315

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 6319

This theorem is referenced by:  ordelss  6332  ordn2lp  6336  ordelord  6338  tz7.7  6342  ordelssne  6343  ordin  6346  ordtr1  6360  orduniss  6415  ontr  6427  dford5  7729  ordsuci  7753  ordunisuc  7774  limsuc  7791  trom  7817  dfrecs3  8304  tz7.44-2  8338  cantnflt  9583  cantnfp1lem3  9591  cantnflem1b  9597  cantnflem1  9600  cnfcom  9611  axdc3lem2  10363  inar1  10688  efgmnvl  19645  bnj967  35080  dford3  43307  limsuc2  43320  ordsssucim  43681  ordelordALT  44815  onfrALTlem2  44824  ordelordALTVD  45144  onfrALTlem2VD  45166  iunord  49958