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

Theorem dftr2 5140
 Description: An alternate way of defining a transitive class. Exercise 7 of [TakeutiZaring] p. 40. (Contributed by NM, 24-Apr-1994.)
Assertion
Ref Expression
dftr2 (Tr 𝐴 ↔ ∀𝑥𝑦((𝑥𝑦𝑦𝐴) → 𝑥𝐴))
Distinct variable group:   𝑥,𝑦,𝐴

Proof of Theorem dftr2
StepHypRef Expression
1 dfss2 3878 . 2 ( 𝐴𝐴 ↔ ∀𝑥(𝑥 𝐴𝑥𝐴))
2 df-tr 5139 . 2 (Tr 𝐴 𝐴𝐴)
3 19.23v 1943 . . . 4 (∀𝑦((𝑥𝑦𝑦𝐴) → 𝑥𝐴) ↔ (∃𝑦(𝑥𝑦𝑦𝐴) → 𝑥𝐴))
4 eluni 4801 . . . . 5 (𝑥 𝐴 ↔ ∃𝑦(𝑥𝑦𝑦𝐴))
54imbi1i 353 . . . 4 ((𝑥 𝐴𝑥𝐴) ↔ (∃𝑦(𝑥𝑦𝑦𝐴) → 𝑥𝐴))
63, 5bitr4i 281 . . 3 (∀𝑦((𝑥𝑦𝑦𝐴) → 𝑥𝐴) ↔ (𝑥 𝐴𝑥𝐴))
76albii 1821 . 2 (∀𝑥𝑦((𝑥𝑦𝑦𝐴) → 𝑥𝐴) ↔ ∀𝑥(𝑥 𝐴𝑥𝐴))
81, 2, 73bitr4i 306 1 (Tr 𝐴 ↔ ∀𝑥𝑦((𝑥𝑦𝑦𝐴) → 𝑥𝐴))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1536  ∃wex 1781   ∈ wcel 2111   ⊆ wss 3858  ∪ cuni 4798  Tr wtr 5138 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3865  df-ss 3875  df-uni 4799  df-tr 5139 This theorem is referenced by:  dftr5  5141  trel  5145  ordelord  6191  suctr  6252  ordom  7588  hartogs  9041  card2on  9051  trcl  9203  tskwe  9412  ondomon  10023  dftr6  33233  elpotr  33273  nosupno  33471  noinfno  33486  hftr  34033  dford4  40343  mnutrd  41361  tratrb  41615  trsbc  41619  truniALT  41620  sspwtr  41900  sspwtrALT  41901  sspwtrALT2  41902  pwtrVD  41903  pwtrrVD  41904  suctrALT  41905  suctrALT2VD  41915  suctrALT2  41916  tratrbVD  41940  trsbcVD  41956  truniALTVD  41957  trintALTVD  41959  trintALT  41960  suctrALTcf  42001  suctrALTcfVD  42002  suctrALT3  42003
 Copyright terms: Public domain W3C validator