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

Theorem dftr3 5262
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 𝐴 ↔ ∀𝑥𝐴 𝑥𝐴)
Distinct variable group:   𝑥,𝐴

Proof of Theorem dftr3
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 dftr5 5260 . 2 (Tr 𝐴 ↔ ∀𝑥𝐴𝑦𝑥 𝑦𝐴)
2 dfss3 3963 . . 3 (𝑥𝐴 ↔ ∀𝑦𝑥 𝑦𝐴)
32ralbii 3085 . 2 (∀𝑥𝐴 𝑥𝐴 ↔ ∀𝑥𝐴𝑦𝑥 𝑦𝐴)
41, 3bitr4i 278 1 (Tr 𝐴 ↔ ∀𝑥𝐴 𝑥𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wcel 2098  wral 3053  wss 3941  Tr wtr 5256
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695
This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-ral 3054  df-v 3468  df-in 3948  df-ss 3958  df-uni 4901  df-tr 5257
This theorem is referenced by:  trss  5267  trin  5268  triun  5271  triin  5273  tron  6378  ssorduni  7760  sucexeloniOLD  7792  suceloniOLD  7794  dfrecs3  8368  dfrecs3OLD  8369  ordtypelem2  9511  tcwf  9875  itunitc  10413  wunex2  10730  wfgru  10808  nadd2rabtr  42683
  Copyright terms: Public domain W3C validator