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

Theorem treq 4536
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 4242 . . . 4  |-  ( A  =  B  ->  U. A  =  U. B )
21sseq1d 3516 . . 3  |-  ( A  =  B  ->  ( U. A  C_  A  <->  U. B  C_  A ) )
3 sseq2 3511 . . 3  |-  ( A  =  B  ->  ( U. B  C_  A  <->  U. B  C_  B ) )
42, 3bitrd 253 . 2  |-  ( A  =  B  ->  ( U. A  C_  A  <->  U. B  C_  B ) )
5 df-tr 4531 . 2  |-  ( Tr  A  <->  U. A  C_  A
)
6 df-tr 4531 . 2  |-  ( Tr  B  <->  U. B  C_  B
)
74, 5, 63bitr4g 288 1  |-  ( A  =  B  ->  ( Tr  A  <->  Tr  B )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1383    C_ wss 3461   U.cuni 4234   Tr wtr 4530
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rex 2799  df-in 3468  df-ss 3475  df-uni 4235  df-tr 4531
This theorem is referenced by:  truni  4544  ordeq  4875  trcl  8162  tz9.1  8163  tz9.1c  8164  tctr  8174  tcmin  8175  tc2  8176  r1tr  8197  r1elssi  8226  tcrank  8305  iswun  9085  tskr1om2  9149  elgrug  9173  grutsk  9203  dfon2lem1  29191  dfon2lem3  29193  dfon2lem4  29194  dfon2lem5  29195  dfon2lem6  29196  dfon2lem7  29197  dfon2lem8  29198  dfon2  29200  dford3lem1  30944  dford3lem2  30945
  Copyright terms: Public domain W3C validator