Theorem ordtr 6173

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

Syntax hints:   → wi 4  Tr wtr 5136   E cep 5429   We wwe 5477  Ord word 6158

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 210  df-an 400  df-ord 6162

This theorem is referenced by:  ordelss  6175  ordn2lp  6179  ordelord  6181  tz7.7  6185  ordelssne  6186  ordin  6189  ordtr1  6202  orduniss  6253  ontrci  6264  ordunisuc  7527  onuninsuci  7535  limsuc  7544  ordom  7569  elnn  7570  omsinds  7580  dfrecs3  7992  tz7.44-2  8026  cantnflt  9119  cantnfp1lem3  9127  cantnflem1b  9133  cantnflem1  9136  cnfcom  9147  axdc3lem2  9862  inar1  10186  efgmnvl  18832  bnj967  32327  dford5  33070  dford3  39969  limsuc2  39985  ordelordALT  41243  onfrALTlem2  41252  ordelordALTVD  41573  onfrALTlem2VD  41595  iunord  45206