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

Theorem treq 4917
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 4602 . . . 4 (𝐴 = 𝐵 𝐴 = 𝐵)
21sseq1d 3792 . . 3 (𝐴 = 𝐵 → ( 𝐴𝐴 𝐵𝐴))
3 sseq2 3787 . . 3 (𝐴 = 𝐵 → ( 𝐵𝐴 𝐵𝐵))
42, 3bitrd 270 . 2 (𝐴 = 𝐵 → ( 𝐴𝐴 𝐵𝐵))
5 df-tr 4912 . 2 (Tr 𝐴 𝐴𝐴)
6 df-tr 4912 . 2 (Tr 𝐵 𝐵𝐵)
74, 5, 63bitr4g 305 1 (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197   = wceq 1652  wss 3732   cuni 4594  Tr wtr 4911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-rex 3061  df-in 3739  df-ss 3746  df-uni 4595  df-tr 4912
This theorem is referenced by:  truni  4925  trint  4927  ordeq  5915  trcl  8819  tz9.1  8820  tz9.1c  8821  tctr  8831  tcmin  8832  tc2  8833  r1tr  8854  r1elssi  8883  tcrank  8962  iswun  9779  tskr1om2  9843  elgrug  9867  grutsk  9897  dfon2lem1  32063  dfon2lem3  32065  dfon2lem4  32066  dfon2lem5  32067  dfon2lem6  32068  dfon2lem7  32069  dfon2lem8  32070  dfon2  32072  dford3lem1  38202  dford3lem2  38203
  Copyright terms: Public domain W3C validator