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

Theorem treq 5175
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 4845 . . . 4 (𝐴 = 𝐵 𝐴 = 𝐵)
21sseq1d 4002 . . 3 (𝐴 = 𝐵 → ( 𝐴𝐴 𝐵𝐴))
3 sseq2 3997 . . 3 (𝐴 = 𝐵 → ( 𝐵𝐴 𝐵𝐵))
42, 3bitrd 280 . 2 (𝐴 = 𝐵 → ( 𝐴𝐴 𝐵𝐵))
5 df-tr 5170 . 2 (Tr 𝐴 𝐴𝐴)
6 df-tr 5170 . 2 (Tr 𝐵 𝐵𝐵)
74, 5, 63bitr4g 315 1 (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1530  wss 3940   cuni 4837  Tr wtr 5169
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-rex 3149  df-in 3947  df-ss 3956  df-uni 4838  df-tr 5170
This theorem is referenced by:  truni  5183  trint  5185  ordeq  6197  trcl  9164  tz9.1  9165  tz9.1c  9166  tctr  9176  tcmin  9177  tc2  9178  r1tr  9199  r1elssi  9228  tcrank  9307  iswun  10120  tskr1om2  10184  elgrug  10208  grutsk  10238  dfon2lem1  32931  dfon2lem3  32933  dfon2lem4  32934  dfon2lem5  32935  dfon2lem6  32936  dfon2lem7  32937  dfon2lem8  32938  dfon2  32940  dford3lem1  39507  dford3lem2  39508
  Copyright terms: Public domain W3C validator