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

Theorem treq 5274
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 4920 . . . 4 (𝐴 = 𝐵 𝐴 = 𝐵)
21sseq1d 4014 . . 3 (𝐴 = 𝐵 → ( 𝐴𝐴 𝐵𝐴))
3 sseq2 4009 . . 3 (𝐴 = 𝐵 → ( 𝐵𝐴 𝐵𝐵))
42, 3bitrd 279 . 2 (𝐴 = 𝐵 → ( 𝐴𝐴 𝐵𝐵))
5 df-tr 5267 . 2 (Tr 𝐴 𝐴𝐴)
6 df-tr 5267 . 2 (Tr 𝐵 𝐵𝐵)
74, 5, 63bitr4g 314 1 (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1542  wss 3949   cuni 4909  Tr wtr 5266
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 3477  df-in 3956  df-ss 3966  df-uni 4910  df-tr 5267
This theorem is referenced by:  truni  5282  trint  5284  ordeq  6372  trcl  9723  tz9.1  9724  tz9.1c  9725  tctr  9735  tcmin  9736  tc2  9737  r1tr  9771  r1elssi  9800  tcrank  9879  iswun  10699  tskr1om2  10763  elgrug  10787  grutsk  10817  dfon2lem1  34755  dfon2lem3  34757  dfon2lem4  34758  dfon2lem5  34759  dfon2lem6  34760  dfon2lem7  34761  dfon2lem8  34762  dfon2  34764  dford3lem1  41765  dford3lem2  41766  nadd1rabtr  42138
  Copyright terms: Public domain W3C validator