Theorem ordtr 6320

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

Syntax hints:   → wi 4  Tr wtr 5196   E cep 5513   We wwe 5566  Ord word 6305

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 6309

This theorem is referenced by:  ordelss  6322  ordn2lp  6326  ordelord  6328  tz7.7  6332  ordelssne  6333  ordin  6336  ordtr1  6350  orduniss  6405  ontr  6417  dford5  7717  ordsuci  7741  ordunisuc  7762  limsuc  7779  trom  7805  dfrecs3  8292  tz7.44-2  8326  cantnflt  9562  cantnfp1lem3  9570  cantnflem1b  9576  cantnflem1  9579  cnfcom  9590  axdc3lem2  10342  inar1  10666  efgmnvl  19626  bnj967  34957  dford3  43120  limsuc2  43133  ordsssucim  43494  ordelordALT  44629  onfrALTlem2  44638  ordelordALTVD  44958  onfrALTlem2VD  44980  iunord  49776