Theorem ordtr 5654

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

Syntax hints:   → wi 4  Tr wtr 4680   E cep 4947   We wwe 4996  Ord word 5639

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 196  df-an 385  df-ord 5643

This theorem is referenced by:  ordelss  5656  ordn2lp  5660  ordelord  5662  tz7.7  5666  ordelssne  5667  ordin  5670  ordtr1  5684  orduniss  5738  ontrci  5750  ordunisuc  6924  onuninsuci  6932  limsuc  6941  ordom  6966  elnn  6967  omsinds  6976  dfrecs3  7356  tz7.44-2  7390  cantnflt  8452  cantnfp1lem3  8460  cantnflem1b  8466  cantnflem1  8469  cnfcom  8480  axdc3lem2  9156  inar1  9476  efgmnvl  17950  bnj967  30269  dford3  36613  limsuc2  36629  ordelordALT  37768  onfrALTlem2  37782  ordelordALTVD  38125  onfrALTlem2VD  38147  iunord  42220