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

Theorem dftr2 4515
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 3433 . 2  |-  ( U. A  C_  A  <->  A. x
( x  e.  U. A  ->  x  e.  A
) )
2 df-tr 4514 . 2  |-  ( Tr  A  <->  U. A  C_  A
)
3 19.23v 1829 . . . 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 4215 . . . . 5  |-  ( x  e.  U. A  <->  E. y
( x  e.  y  /\  y  e.  A
) )
54imbi1i 331 . . . 4  |-  ( ( x  e.  U. A  ->  x  e.  A )  <-> 
( E. y ( x  e.  y  /\  y  e.  A )  ->  x  e.  A ) )
63, 5bitr4i 260 . . 3  |-  ( A. y ( ( x  e.  y  /\  y  e.  A )  ->  x  e.  A )  <->  ( x  e.  U. A  ->  x  e.  A ) )
76albii 1702 . 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 285 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 189    /\ wa 375   A.wal 1453   E.wex 1674    e. wcel 1898    C_ wss 3416   U.cuni 4212   Tr wtr 4513
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-in 3423  df-ss 3430  df-uni 4213  df-tr 4514
This theorem is referenced by:  dftr5  4516  trel  4520  ordelord  5468  suctr  5529  ordom  6733  hartogs  8090  card2on  8100  trcl  8243  tskwe  8415  ondomon  9019  dftr6  30440  elpotr  30477  hftr  30999  dford4  35930  tratrb  36942  trsbc  36946  truniALT  36947  sspwtr  37250  sspwtrALT  37251  sspwtrALT2  37260  pwtrVD  37261  pwtrrVD  37262  suctrALT  37263  suctrALT2VD  37273  suctrALT2  37274  tratrbVD  37299  trsbcVD  37315  truniALTVD  37316  trintALTVD  37318  trintALT  37319  suctrALTcf  37360  suctrALTcfVD  37361  suctrALT3  37362
  Copyright terms: Public domain W3C validator