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

Theorem ordtr 4143
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 4132 . 2 (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥𝐴 Tr 𝑥))
21simplbi 263 1 (Ord 𝐴 → Tr 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4  wral 2323  Tr wtr 3882  Ord word 4127
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103
This theorem depends on definitions:  df-bi 114  df-iord 4131
This theorem is referenced by:  ordelss  4144  ordin  4150  ordtr1  4153  orduniss  4190  ontrci  4192  ordon  4240  ordsucim  4254  ordsucss  4258  onsucsssucr  4263  onintonm  4271  ordsucunielexmid  4284  ordn2lp  4297  onsucuni2  4316  nlimsucg  4318  ordpwsucss  4319  tfrexlem  5979
  Copyright terms: Public domain W3C validator