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

Theorem dftr2 4471
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 3429 . 2  |-  ( U. A  C_  A  <->  A. x
( x  e.  U. A  ->  x  e.  A
) )
2 df-tr 4470 . 2  |-  ( Tr  A  <->  U. A  C_  A
)
3 19.23v 1911 . . . 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 4178 . . . . 5  |-  ( x  e.  U. A  <->  E. y
( x  e.  y  /\  y  e.  A
) )
54imbi1i 325 . . . 4  |-  ( ( x  e.  U. A  ->  x  e.  A )  <-> 
( E. y ( x  e.  y  /\  y  e.  A )  ->  x  e.  A ) )
63, 5bitr4i 252 . . 3  |-  ( A. y ( ( x  e.  y  /\  y  e.  A )  ->  x  e.  A )  <->  ( x  e.  U. A  ->  x  e.  A ) )
76albii 1611 . 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 277 1  |-  ( Tr  A  <->  A. x A. y
( ( x  e.  y  /\  y  e.  A )  ->  x  e.  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369   A.wal 1368   E.wex 1587    e. wcel 1757    C_ wss 3412   U.cuni 4175   Tr wtr 4469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-v 3056  df-in 3419  df-ss 3426  df-uni 4176  df-tr 4470
This theorem is referenced by:  dftr5  4472  trel  4476  ordelord  4825  suctr  4886  ordom  6571  hartogs  7845  card2on  7856  trcl  8035  tskwe  8207  ondomon  8814  dftr6  27680  elpotr  27714  hftr  28340  dford4  29502  tratrb  31524  trsbc  31529  truniALT  31530  sspwtr  31837  sspwtrALT  31838  sspwtrALT2  31841  pwtrVD  31842  pwtrrVD  31843  suctrALT  31844  suctrALT2VD  31854  suctrALT2  31855  tratrbVD  31879  trsbcVD  31895  truniALTVD  31896  trintALTVD  31898  trintALT  31899  suctrALTcf  31940  suctrALTcfVD  31941  suctrALT3  31942
  Copyright terms: Public domain W3C validator