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

Theorem treq 5234
Description: Equality theorem for the transitive class predicate. (Contributed by NM, 17-Sep-1993.)
Assertion
Ref Expression
treq (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵))

Proof of Theorem treq
StepHypRef Expression
1 unieq 4880 . . . 4 (𝐴 = 𝐵 𝐴 = 𝐵)
21sseq1d 3979 . . 3 (𝐴 = 𝐵 → ( 𝐴𝐴 𝐵𝐴))
3 sseq2 3974 . . 3 (𝐴 = 𝐵 → ( 𝐵𝐴 𝐵𝐵))
42, 3bitrd 279 . 2 (𝐴 = 𝐵 → ( 𝐴𝐴 𝐵𝐵))
5 df-tr 5227 . 2 (Tr 𝐴 𝐴𝐴)
6 df-tr 5227 . 2 (Tr 𝐵 𝐵𝐵)
74, 5, 63bitr4g 314 1 (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1542  wss 3914   cuni 4869  Tr wtr 5226
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3449  df-in 3921  df-ss 3931  df-uni 4870  df-tr 5227
This theorem is referenced by:  truni  5242  trint  5244  ordeq  6328  trcl  9672  tz9.1  9673  tz9.1c  9674  tctr  9684  tcmin  9685  tc2  9686  r1tr  9720  r1elssi  9749  tcrank  9828  iswun  10648  tskr1om2  10712  elgrug  10736  grutsk  10766  dfon2lem1  34421  dfon2lem3  34423  dfon2lem4  34424  dfon2lem5  34425  dfon2lem6  34426  dfon2lem7  34427  dfon2lem8  34428  dfon2  34430  dford3lem1  41397  dford3lem2  41398  nadd1rabtr  41751
  Copyright terms: Public domain W3C validator