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

Theorem treq 4503
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 4206 . . . 4  |-  ( A  =  B  ->  U. A  =  U. B )
21sseq1d 3459 . . 3  |-  ( A  =  B  ->  ( U. A  C_  A  <->  U. B  C_  A ) )
3 sseq2 3454 . . 3  |-  ( A  =  B  ->  ( U. B  C_  A  <->  U. B  C_  B ) )
42, 3bitrd 257 . 2  |-  ( A  =  B  ->  ( U. A  C_  A  <->  U. B  C_  B ) )
5 df-tr 4498 . 2  |-  ( Tr  A  <->  U. A  C_  A
)
6 df-tr 4498 . 2  |-  ( Tr  B  <->  U. B  C_  B
)
74, 5, 63bitr4g 292 1  |-  ( A  =  B  ->  ( Tr  A  <->  Tr  B )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    = wceq 1444    C_ wss 3404   U.cuni 4198   Tr wtr 4497
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-rex 2743  df-in 3411  df-ss 3418  df-uni 4199  df-tr 4498
This theorem is referenced by:  truni  4511  ordeq  5430  trcl  8212  tz9.1  8213  tz9.1c  8214  tctr  8224  tcmin  8225  tc2  8226  r1tr  8247  r1elssi  8276  tcrank  8355  iswun  9129  tskr1om2  9193  elgrug  9217  grutsk  9247  dfon2lem1  30429  dfon2lem3  30431  dfon2lem4  30432  dfon2lem5  30433  dfon2lem6  30434  dfon2lem7  30435  dfon2lem8  30436  dfon2  30438  dford3lem1  35881  dford3lem2  35882
  Copyright terms: Public domain W3C validator