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

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

Proof of Theorem dftr2
StepHypRef Expression
1 df-ss 3967 . 2 ( 𝐴𝐴 ↔ ∀𝑥(𝑥 𝐴𝑥𝐴))
2 df-tr 5259 . 2 (Tr 𝐴 𝐴𝐴)
3 19.23v 1941 . . . 4 (∀𝑦((𝑥𝑦𝑦𝐴) → 𝑥𝐴) ↔ (∃𝑦(𝑥𝑦𝑦𝐴) → 𝑥𝐴))
4 eluni 4909 . . . . 5 (𝑥 𝐴 ↔ ∃𝑦(𝑥𝑦𝑦𝐴))
54imbi1i 349 . . . 4 ((𝑥 𝐴𝑥𝐴) ↔ (∃𝑦(𝑥𝑦𝑦𝐴) → 𝑥𝐴))
63, 5bitr4i 278 . . 3 (∀𝑦((𝑥𝑦𝑦𝐴) → 𝑥𝐴) ↔ (𝑥 𝐴𝑥𝐴))
76albii 1818 . 2 (∀𝑥𝑦((𝑥𝑦𝑦𝐴) → 𝑥𝐴) ↔ ∀𝑥(𝑥 𝐴𝑥𝐴))
81, 2, 73bitr4i 303 1 (Tr 𝐴 ↔ ∀𝑥𝑦((𝑥𝑦𝑦𝐴) → 𝑥𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wal 1537  wex 1778  wcel 2107  wss 3950   cuni 4906  Tr wtr 5258
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-ss 3967  df-uni 4907  df-tr 5259
This theorem is referenced by:  dftr2c  5261  dftr5OLD  5263  trel  5267  ordelord  6405  suctr  6469  trom  7897  hartogs  9585  card2on  9595  trcl  9769  tskwe  9991  ondomon  10604  nosupno  27749  noinfno  27764  dftr6  35752  elpotr  35783  hftr  36184  dford4  43046  mnutrd  44304  tratrb  44561  trsbc  44565  truniALT  44566  sspwtr  44846  sspwtrALT  44847  sspwtrALT2  44848  pwtrVD  44849  pwtrrVD  44850  suctrALT  44851  suctrALT2VD  44861  suctrALT2  44862  tratrbVD  44886  trsbcVD  44902  truniALTVD  44903  trintALTVD  44905  trintALT  44906  suctrALTcf  44947  suctrALTcfVD  44948  suctrALT3  44949
  Copyright terms: Public domain W3C validator