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

Theorem dftr2 4552
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 3488 . 2  |-  ( U. A  C_  A  <->  A. x
( x  e.  U. A  ->  x  e.  A
) )
2 df-tr 4551 . 2  |-  ( Tr  A  <->  U. A  C_  A
)
3 19.23v 1761 . . . 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 4254 . . . . 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 1641 . 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 1393   E.wex 1613    e. wcel 1819    C_ wss 3471   U.cuni 4251   Tr wtr 4550
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3478  df-ss 3485  df-uni 4252  df-tr 4551
This theorem is referenced by:  dftr5  4553  trel  4557  ordelord  4909  suctr  4970  ordom  6708  hartogs  7987  card2on  7998  trcl  8176  tskwe  8348  ondomon  8955  dftr6  29376  elpotr  29409  hftr  30023  dford4  31154  tratrb  33429  trsbc  33433  truniALT  33434  sspwtr  33741  sspwtrALT  33742  sspwtrALT2  33745  pwtrVD  33746  pwtrrVD  33747  suctrALT  33748  suctrALT2VD  33758  suctrALT2  33759  tratrbVD  33783  trsbcVD  33799  truniALTVD  33800  trintALTVD  33802  trintALT  33803  suctrALTcf  33844  suctrALTcfVD  33845  suctrALT3  33846
  Copyright terms: Public domain W3C validator