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

Theorem dftr2 5267
Description: An alternate way of defining a transitive class. Exercise 7 of [TakeutiZaring] p. 40. Using dftr2c 5268 instead may avoid dependences on ax-11 2155. (Contributed by NM, 24-Apr-1994.)
Assertion
Ref Expression
dftr2 (Tr 𝐴 ↔ ∀𝑥𝑦((𝑥𝑦𝑦𝐴) → 𝑥𝐴))
Distinct variable group:   𝑥,𝑦,𝐴

Proof of Theorem dftr2
StepHypRef Expression
1 df-ss 3980 . 2 ( 𝐴𝐴 ↔ ∀𝑥(𝑥 𝐴𝑥𝐴))
2 df-tr 5266 . 2 (Tr 𝐴 𝐴𝐴)
3 19.23v 1940 . . . 4 (∀𝑦((𝑥𝑦𝑦𝐴) → 𝑥𝐴) ↔ (∃𝑦(𝑥𝑦𝑦𝐴) → 𝑥𝐴))
4 eluni 4915 . . . . 5 (𝑥 𝐴 ↔ ∃𝑦(𝑥𝑦𝑦𝐴))
54imbi1i 349 . . . 4 ((𝑥 𝐴𝑥𝐴) ↔ (∃𝑦(𝑥𝑦𝑦𝐴) → 𝑥𝐴))
63, 5bitr4i 278 . . 3 (∀𝑦((𝑥𝑦𝑦𝐴) → 𝑥𝐴) ↔ (𝑥 𝐴𝑥𝐴))
76albii 1816 . 2 (∀𝑥𝑦((𝑥𝑦𝑦𝐴) → 𝑥𝐴) ↔ ∀𝑥(𝑥 𝐴𝑥𝐴))
81, 2, 73bitr4i 303 1 (Tr 𝐴 ↔ ∀𝑥𝑦((𝑥𝑦𝑦𝐴) → 𝑥𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wal 1535  wex 1776  wcel 2106  wss 3963   cuni 4912  Tr wtr 5265
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-ss 3980  df-uni 4913  df-tr 5266
This theorem is referenced by:  dftr2c  5268  dftr5OLD  5270  trel  5274  ordelord  6408  suctr  6472  trom  7896  hartogs  9582  card2on  9592  trcl  9766  tskwe  9988  ondomon  10601  nosupno  27763  noinfno  27778  dftr6  35731  elpotr  35763  hftr  36164  dford4  43018  mnutrd  44276  tratrb  44534  trsbc  44538  truniALT  44539  sspwtr  44819  sspwtrALT  44820  sspwtrALT2  44821  pwtrVD  44822  pwtrrVD  44823  suctrALT  44824  suctrALT2VD  44834  suctrALT2  44835  tratrbVD  44859  trsbcVD  44875  truniALTVD  44876  trintALTVD  44878  trintALT  44879  suctrALTcf  44920  suctrALTcfVD  44921  suctrALT3  44922
  Copyright terms: Public domain W3C validator