Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  dftr3 Unicode version

Theorem dftr3 4133
 Description: An alternate way of defining a transitive class. Definition 7.1 of [TakeutiZaring] p. 35. (Contributed by NM, 29-Aug-1993.)
Assertion
Ref Expression
dftr3
Distinct variable group:   ,

Proof of Theorem dftr3
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 dftr5 4132 . 2
2 dfss3 3183 . . 3
32ralbii 2580 . 2
41, 3bitr4i 243 1
 Colors of variables: wff set class Syntax hints:   wb 176   wcel 1696  wral 2556   wss 3165   wtr 4129 This theorem is referenced by:  trss  4138  trin  4139  triun  4142  trint  4144  tron  4431  ssorduni  4593  suceloni  4620  ordtypelem2  7250  tcwf  7569  itunitc  8063  wunex2  8376  wfgru  8454  gruina  8456  grur1  8458  tfrALTlem  24347  celsor  25214 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-v 2803  df-in 3172  df-ss 3179  df-uni 3844  df-tr 4130
 Copyright terms: Public domain W3C validator