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

Theorem dftr2 4089
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 3144 . 2  |-  ( U. A  C_  A  <->  A. x
( x  e.  U. A  ->  x  e.  A
) )
2 df-tr 4088 . 2  |-  ( Tr  A  <->  U. A  C_  A
)
3 19.23v 2022 . . . 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 3804 . . . . 5  |-  ( x  e.  U. A  <->  E. y
( x  e.  y  /\  y  e.  A
) )
54imbi1i 317 . . . 4  |-  ( ( x  e.  U. A  ->  x  e.  A )  <-> 
( E. y ( x  e.  y  /\  y  e.  A )  ->  x  e.  A ) )
63, 5bitr4i 245 . . 3  |-  ( A. y ( ( x  e.  y  /\  y  e.  A )  ->  x  e.  A )  <->  ( x  e.  U. A  ->  x  e.  A ) )
76albii 1554 . 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 270 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 6    <-> wb 178    /\ wa 360   A.wal 1532   E.wex 1537    e. wcel 1621    C_ wss 3127   U.cuni 3801   Tr wtr 4087
This theorem is referenced by:  dftr5  4090  trel  4094  ordelord  4386  suctr  4447  trsuc2OLD  4449  ordom  4637  hartogs  7227  card2on  7236  trcl  7378  tskwe  7551  ondomon  8153  dftr6  23479  elpotr  23507  hftr  24188  dford4  26490  tratrb  27435  trsbc  27440  truniALT  27441  sspwtr  27728  sspwtrALT  27729  sspwtrALT2  27730  pwtrVD  27731  pwtrOLD  27732  pwtrrVD  27733  pwtrrOLD  27734  suctrALT2VD  27745  suctrALT2  27746  tratrbVD  27770  trsbcVD  27786  truniALTVD  27787  trintALTVD  27789  trintALT  27790  suctrALTcf  27831  suctrALTcfVD  27832  suctrALT3  27833  suctrALT4  27837
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-v 2765  df-in 3134  df-ss 3141  df-uni 3802  df-tr 4088
  Copyright terms: Public domain W3C validator