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

Theorem dftr2 4115
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  A  <->  A. x A. y
( ( x  e.  y  /\  y  e.  A )  ->  x  e.  A ) )
Distinct variable group:    x, y, A

Proof of Theorem dftr2
StepHypRef Expression
1 dfss2 3169 . 2  |-  ( U. A  C_  A  <->  A. x
( x  e.  U. A  ->  x  e.  A
) )
2 df-tr 4114 . 2  |-  ( Tr  A  <->  U. A  C_  A
)
3 19.23v 1832 . . . 4  |-  ( A. y ( ( x  e.  y  /\  y  e.  A )  ->  x  e.  A )  <->  ( E. y ( x  e.  y  /\  y  e.  A )  ->  x  e.  A ) )
4 eluni 3830 . . . . 5  |-  ( x  e.  U. A  <->  E. y
( x  e.  y  /\  y  e.  A
) )
54imbi1i 315 . . . 4  |-  ( ( x  e.  U. A  ->  x  e.  A )  <-> 
( E. y ( x  e.  y  /\  y  e.  A )  ->  x  e.  A ) )
63, 5bitr4i 243 . . 3  |-  ( A. y ( ( x  e.  y  /\  y  e.  A )  ->  x  e.  A )  <->  ( x  e.  U. A  ->  x  e.  A ) )
76albii 1553 . 2  |-  ( A. x A. y ( ( x  e.  y  /\  y  e.  A )  ->  x  e.  A )  <->  A. x ( x  e. 
U. A  ->  x  e.  A ) )
81, 2, 73bitr4i 268 1  |-  ( Tr  A  <->  A. x A. y
( ( x  e.  y  /\  y  e.  A )  ->  x  e.  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358   A.wal 1527   E.wex 1528    e. wcel 1684    C_ wss 3152   U.cuni 3827   Tr wtr 4113
This theorem is referenced by:  dftr5  4116  trel  4120  ordelord  4414  suctr  4475  trsuc2OLD  4477  ordom  4665  hartogs  7259  card2on  7268  trcl  7410  tskwe  7583  ondomon  8185  dftr6  24107  elpotr  24137  hftr  24812  dford4  27122  tratrb  28299  trsbc  28304  truniALT  28305  sspwtr  28595  sspwtrALT  28596  sspwtrALT2  28597  pwtrVD  28598  pwtrOLD  28599  pwtrrVD  28600  pwtrrOLD  28601  suctrALT2VD  28612  suctrALT2  28613  tratrbVD  28637  trsbcVD  28653  truniALTVD  28654  trintALTVD  28656  trintALT  28657  suctrALTcf  28698  suctrALTcfVD  28699  suctrALT3  28700  suctrALT4  28704
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-ss 3166  df-uni 3828  df-tr 4114
  Copyright terms: Public domain W3C validator