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

Theorem treq 4200
Description: Equality theorem for the transitive class predicate. (Contributed by NM, 17-Sep-1993.)
Assertion
Ref Expression
treq  |-  ( A  =  B  ->  ( Tr  A  <->  Tr  B )
)

Proof of Theorem treq
StepHypRef Expression
1 unieq 3917 . . . 4  |-  ( A  =  B  ->  U. A  =  U. B )
21sseq1d 3281 . . 3  |-  ( A  =  B  ->  ( U. A  C_  A  <->  U. B  C_  A ) )
3 sseq2 3276 . . 3  |-  ( A  =  B  ->  ( U. B  C_  A  <->  U. B  C_  B ) )
42, 3bitrd 244 . 2  |-  ( A  =  B  ->  ( U. A  C_  A  <->  U. B  C_  B ) )
5 df-tr 4195 . 2  |-  ( Tr  A  <->  U. A  C_  A
)
6 df-tr 4195 . 2  |-  ( Tr  B  <->  U. B  C_  B
)
74, 5, 63bitr4g 279 1  |-  ( A  =  B  ->  ( Tr  A  <->  Tr  B )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1642    C_ wss 3228   U.cuni 3908   Tr wtr 4194
This theorem is referenced by:  truni  4208  ordeq  4481  trsuc2OLD  4559  trcl  7500  tz9.1  7501  tz9.1c  7502  tctr  7515  tcmin  7516  tc2  7517  r1tr  7538  r1elssi  7567  tcrank  7644  iswun  8416  tskr1om2  8480  elgrug  8504  grutsk  8534  dfon2lem1  24697  dfon2lem3  24699  dfon2lem4  24700  dfon2lem5  24701  dfon2lem6  24702  dfon2lem7  24703  dfon2lem8  24704  dfon2  24706  dford3lem1  26442  dford3lem2  26443
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-rex 2625  df-in 3235  df-ss 3242  df-uni 3909  df-tr 4195
  Copyright terms: Public domain W3C validator