Theorem ordtr 4897

Description: An ordinal class is transitive. (Contributed by NM, 3-Apr-1994.)

Assertion

Ref	Expression
ordtr

Proof of Theorem ordtr

Step	Hyp	Ref	Expression
1		df-ord 4886	. 2
2	1	simplbi 460	1

Syntax hints:  ->wi 4  Trwtr 4545  cep 4794  Wewwe 4842  Ordword 4882

This theorem is referenced by:  ordelss  4899  ordn2lp  4903  ordelord  4905  tz7.7  4909  ordelssne  4910  ordin  4913  ordtr1  4926  orduniss  4977  ontrci  4988  ordunisuc  6667  onuninsuci  6675  limsuc  6684  ordom  6709  elnn  6710  tz7.44-2  7092  cantnflt  8112  cantnfp1lem3  8120  cantnflem1b  8126  cantnflem1  8129  cantnfltOLD  8142  cantnfp1lem3OLD  8146  cantnflem1bOLD  8149  cantnflem1OLD  8152  cnfcom  8165  cnfcomOLD  8173  axdc3lem2  8852  inar1  9174  efgmnvl  16732  omsinds  29299  dford3  30970  limsuc2  30986  ordelordALT  33308  onfrALTlem2  33318  ordelordALTVD  33667  onfrALTlem2VD  33689  bnj967  34003

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 185  df-an 371  df-ord 4886