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

Theorem dftr2 4547
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
Distinct variable group:   , ,

Proof of Theorem dftr2
StepHypRef Expression
1 dfss2 3492 . 2
2 df-tr 4546 . 2
3 19.23v 1760 . . . 4
4 eluni 4252 . . . . 5
54imbi1i 325 . . . 4
63, 5bitr4i 252 . . 3
76albii 1640 . 2
81, 2, 73bitr4i 277 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  A.wal 1393  E.wex 1612  e.wcel 1818  C_wss 3475  U.cuni 4249  Trwtr 4545
This theorem is referenced by:  dftr5  4548  trel  4552  ordelord  4905  suctr  4966  ordom  6709  hartogs  7990  card2on  8001  trcl  8180  tskwe  8352  ondomon  8959  dftr6  29179  elpotr  29213  hftr  29839  dford4  30971  tratrb  33307  trsbc  33311  truniALT  33312  sspwtr  33619  sspwtrALT  33620  sspwtrALT2  33623  pwtrVD  33624  pwtrrVD  33625  suctrALT  33626  suctrALT2VD  33636  suctrALT2  33637  tratrbVD  33661  trsbcVD  33677  truniALTVD  33678  trintALTVD  33680  trintALT  33681  suctrALTcf  33722  suctrALTcfVD  33723  suctrALT3  33724
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3482  df-ss 3489  df-uni 4250  df-tr 4546
  Copyright terms: Public domain W3C validator