Theorem ordtr 6349

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

Syntax hints:   → wi 4  Tr wtr 5217   E cep 5540   We wwe 5593  Ord word 6334

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 6338

This theorem is referenced by:  ordelss  6351  ordn2lp  6355  ordelord  6357  tz7.7  6361  ordelssne  6362  ordin  6365  ordtr1  6379  orduniss  6434  ontr  6446  dford5  7763  ordsuci  7787  ordunisuc  7810  limsuc  7828  trom  7854  dfrecs3  8344  tz7.44-2  8378  cantnflt  9632  cantnfp1lem3  9640  cantnflem1b  9646  cantnflem1  9649  cnfcom  9660  axdc3lem2  10411  inar1  10735  efgmnvl  19651  bnj967  34942  dford3  43024  limsuc2  43037  ordsssucim  43398  ordelordALT  44534  onfrALTlem2  44543  ordelordALTVD  44863  onfrALTlem2VD  44885  iunord  49669