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

Theorem dftr2 4131
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 3182 . 2  |-  ( U. A  C_  A  <->  A. x
( x  e.  U. A  ->  x  e.  A
) )
2 df-tr 4130 . 2  |-  ( Tr  A  <->  U. A  C_  A
)
3 19.23v 1844 . . . 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 3846 . . . . 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 1556 . 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 1530   E.wex 1531    e. wcel 1696    C_ wss 3165   U.cuni 3843   Tr wtr 4129
This theorem is referenced by:  dftr5  4132  trel  4136  ordelord  4430  suctr  4491  trsuc2OLD  4493  ordom  4681  hartogs  7275  card2on  7284  trcl  7426  tskwe  7599  ondomon  8201  dftr6  24178  elpotr  24208  hftr  24884  dford4  27225  tratrb  28598  trsbc  28603  truniALT  28604  sspwtr  28911  sspwtrALT  28912  sspwtrALT2  28913  pwtrVD  28914  pwtrOLD  28915  pwtrrVD  28916  pwtrrOLD  28917  suctrALT2VD  28928  suctrALT2  28929  tratrbVD  28953  trsbcVD  28969  truniALTVD  28970  trintALTVD  28972  trintALT  28973  suctrALTcf  29014  suctrALTcfVD  29015  suctrALT3  29016  suctrALT4  29020
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172  df-ss 3179  df-uni 3844  df-tr 4130
  Copyright terms: Public domain W3C validator