Theorem ordtr 6321

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

Syntax hints:   → wi 4  Tr wtr 5199   E cep 5518   We wwe 5571  Ord word 6306

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 6310

This theorem is referenced by:  ordelss  6323  ordn2lp  6327  ordelord  6329  tz7.7  6333  ordelssne  6334  ordin  6337  ordtr1  6351  orduniss  6406  ontr  6418  dford5  7720  ordsuci  7744  ordunisuc  7765  limsuc  7782  trom  7808  dfrecs3  8295  tz7.44-2  8329  cantnflt  9568  cantnfp1lem3  9576  cantnflem1b  9582  cantnflem1  9585  cnfcom  9596  axdc3lem2  10345  inar1  10669  efgmnvl  19593  bnj967  34928  dford3  43021  limsuc2  43034  ordsssucim  43395  ordelordALT  44531  onfrALTlem2  44540  ordelordALTVD  44860  onfrALTlem2VD  44882  iunord  49681