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

Theorem treq 4538
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 4243 . . . 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 4533 . 2  |-  ( Tr  A  <->  U. A  C_  A
)
6 df-tr 4533 . 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 1398    C_ wss 3461   U.cuni 4235   Tr wtr 4532
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rex 2810  df-in 3468  df-ss 3475  df-uni 4236  df-tr 4533
This theorem is referenced by:  truni  4546  ordeq  4874  trcl  8150  tz9.1  8151  tz9.1c  8152  tctr  8162  tcmin  8163  tc2  8164  r1tr  8185  r1elssi  8214  tcrank  8293  iswun  9071  tskr1om2  9135  elgrug  9159  grutsk  9189  dfon2lem1  29458  dfon2lem3  29460  dfon2lem4  29461  dfon2lem5  29462  dfon2lem6  29463  dfon2lem7  29464  dfon2lem8  29465  dfon2  29467  dford3lem1  31210  dford3lem2  31211
  Copyright terms: Public domain W3C validator