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

Theorem treq 5273
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 4923 . . . 4 (𝐴 = 𝐵 𝐴 = 𝐵)
21sseq1d 4027 . . 3 (𝐴 = 𝐵 → ( 𝐴𝐴 𝐵𝐴))
3 sseq2 4022 . . 3 (𝐴 = 𝐵 → ( 𝐵𝐴 𝐵𝐵))
42, 3bitrd 279 . 2 (𝐴 = 𝐵 → ( 𝐴𝐴 𝐵𝐵))
5 df-tr 5266 . 2 (Tr 𝐴 𝐴𝐴)
6 df-tr 5266 . 2 (Tr 𝐵 𝐵𝐵)
74, 5, 63bitr4g 314 1 (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206   = wceq 1537  wss 3963   cuni 4912  Tr wtr 5265
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-ss 3980  df-uni 4913  df-tr 5266
This theorem is referenced by:  truni  5281  trint  5283  ordeq  6393  trcl  9766  tz9.1  9767  tz9.1c  9768  tctr  9778  tcmin  9779  tc2  9780  r1tr  9814  r1elssi  9843  tcrank  9922  iswun  10742  tskr1om2  10806  elgrug  10830  grutsk  10860  dfon2lem1  35765  dfon2lem3  35767  dfon2lem4  35768  dfon2lem5  35769  dfon2lem6  35770  dfon2lem7  35771  dfon2lem8  35772  dfon2  35774  dford3lem1  43015  dford3lem2  43016  nadd1rabtr  43378  wfaxext  44949  wfaxrep  44950
  Copyright terms: Public domain W3C validator