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

Theorem dftr2 4117
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 3171 . 2  |-  ( U. A  C_  A  <->  A. x
( x  e.  U. A  ->  x  e.  A
) )
2 df-tr 4116 . 2  |-  ( Tr  A  <->  U. A  C_  A
)
3 19.23v 1834 . . . 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 3832 . . . . 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 1555 . 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 1529   E.wex 1530    e. wcel 1686    C_ wss 3154   U.cuni 3829   Tr wtr 4115
This theorem is referenced by:  dftr5  4118  trel  4122  ordelord  4416  suctr  4477  trsuc2OLD  4479  ordom  4667  hartogs  7261  card2on  7270  trcl  7412  tskwe  7585  ondomon  8187  dftr6  24109  elpotr  24139  hftr  24814  dford4  27133  tratrb  28355  trsbc  28360  truniALT  28361  sspwtr  28668  sspwtrALT  28669  sspwtrALT2  28670  pwtrVD  28671  pwtrOLD  28672  pwtrrVD  28673  pwtrrOLD  28674  suctrALT2VD  28685  suctrALT2  28686  tratrbVD  28710  trsbcVD  28726  truniALTVD  28727  trintALTVD  28729  trintALT  28730  suctrALTcf  28771  suctrALTcfVD  28772  suctrALT3  28773  suctrALT4  28777
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-v 2792  df-in 3161  df-ss 3168  df-uni 3830  df-tr 4116
  Copyright terms: Public domain W3C validator