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

Theorem dftr3 4270
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  |-  ( Tr  A  <->  A. x  e.  A  x  C_  A )
Distinct variable group:    x, A

Proof of Theorem dftr3
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 dftr5 4269 . 2  |-  ( Tr  A  <->  A. x  e.  A  A. y  e.  x  y  e.  A )
2 dfss3 3302 . . 3  |-  ( x 
C_  A  <->  A. y  e.  x  y  e.  A )
32ralbii 2694 . 2  |-  ( A. x  e.  A  x  C_  A  <->  A. x  e.  A  A. y  e.  x  y  e.  A )
41, 3bitr4i 244 1  |-  ( Tr  A  <->  A. x  e.  A  x  C_  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    e. wcel 1721   A.wral 2670    C_ wss 3284   Tr wtr 4266
This theorem is referenced by:  trss  4275  trin  4276  triun  4279  trint  4281  tron  4568  ssorduni  4729  suceloni  4756  ordtypelem2  7448  tcwf  7767  itunitc  8261  wunex2  8573  wfgru  8651  tfrALTlem  25494
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ral 2675  df-v 2922  df-in 3291  df-ss 3298  df-uni 3980  df-tr 4267
  Copyright terms: Public domain W3C validator