ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ordtr GIF version

Theorem ordtr 4300
Description: An ordinal class is transitive. (Contributed by NM, 3-Apr-1994.)
Assertion
Ref Expression
ordtr (Ord 𝐴 → Tr 𝐴)

Proof of Theorem ordtr
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 dford3 4289 . 2 (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥𝐴 Tr 𝑥))
21simplbi 272 1 (Ord 𝐴 → Tr 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4  wral 2416  Tr wtr 4026  Ord word 4284
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116  df-iord 4288
This theorem is referenced by:  ordelss  4301  ordin  4307  ordtr1  4310  orduniss  4347  ontrci  4349  ordon  4402  ordsucim  4416  ordsucss  4420  onsucsssucr  4425  onintonm  4433  ordsucunielexmid  4446  ordn2lp  4460  onsucuni2  4479  nlimsucg  4481  ordpwsucss  4482  tfrexlem  6231  nnsucuniel  6391  ctmlemr  6993  nnnninf  7023  ctinf  11949  nnsf  13252  peano4nninf  13253  nninfalllemn  13255
  Copyright terms: Public domain W3C validator