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

Theorem dftr3 4077
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
StepHypRef Expression
1 dftr5 4076 . 2  |-  ( Tr  A  <->  A. x  e.  A  A. y  e.  x  y  e.  A )
2 dfss3 3131 . . 3  |-  ( x 
C_  A  <->  A. y  e.  x  y  e.  A )
32ralbii 2540 . 2  |-  ( A. x  e.  A  x  C_  A  <->  A. x  e.  A  A. y  e.  x  y  e.  A )
41, 3bitr4i 245 1  |-  ( Tr  A  <->  A. x  e.  A  x  C_  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    e. wcel 1621   A.wral 2516    C_ wss 3113   Tr wtr 4073
This theorem is referenced by:  trss  4082  trin  4083  triun  4086  trint  4088  tron  4373  ssorduni  4535  suceloni  4562  ordtypelem2  7188  tcwf  7507  itunitc  8001  wunex2  8314  wfgru  8392  gruina  8394  grur1  8396  tfrALTlem  23631  celsor  24463
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ral 2521  df-v 2759  df-in 3120  df-ss 3127  df-uni 3788  df-tr 4074
  Copyright terms: Public domain W3C validator