Theorem ordtr 6398

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

Syntax hints:   → wi 4  Tr wtr 5259   E cep 5583   We wwe 5636  Ord word 6383

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 6387

This theorem is referenced by:  ordelss  6400  ordn2lp  6404  ordelord  6406  tz7.7  6410  ordelssne  6411  ordin  6414  ordtr1  6427  orduniss  6481  ontr  6493  dford5  7804  ordsuci  7828  ordunisuc  7852  limsuc  7870  trom  7896  dfrecs3  8412  dfrecs3OLD  8413  tz7.44-2  8447  cantnflt  9712  cantnfp1lem3  9720  cantnflem1b  9726  cantnflem1  9729  cnfcom  9740  axdc3lem2  10491  inar1  10815  efgmnvl  19732  bnj967  34959  dford3  43040  limsuc2  43053  ordsssucim  43415  ordelordALT  44557  onfrALTlem2  44566  ordelordALTVD  44887  onfrALTlem2VD  44909  iunord  49195