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

Theorem treq 4910
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 4596 . . . 4 (𝐴 = 𝐵 𝐴 = 𝐵)
21sseq1d 3773 . . 3 (𝐴 = 𝐵 → ( 𝐴𝐴 𝐵𝐴))
3 sseq2 3768 . . 3 (𝐴 = 𝐵 → ( 𝐵𝐴 𝐵𝐵))
42, 3bitrd 268 . 2 (𝐴 = 𝐵 → ( 𝐴𝐴 𝐵𝐵))
5 df-tr 4905 . 2 (Tr 𝐴 𝐴𝐴)
6 df-tr 4905 . 2 (Tr 𝐵 𝐵𝐵)
74, 5, 63bitr4g 303 1 (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1632  wss 3715   cuni 4588  Tr wtr 4904
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rex 3056  df-in 3722  df-ss 3729  df-uni 4589  df-tr 4905
This theorem is referenced by:  truni  4919  ordeq  5891  trcl  8779  tz9.1  8780  tz9.1c  8781  tctr  8791  tcmin  8792  tc2  8793  r1tr  8814  r1elssi  8843  tcrank  8922  iswun  9738  tskr1om2  9802  elgrug  9826  grutsk  9856  dfon2lem1  32014  dfon2lem3  32016  dfon2lem4  32017  dfon2lem5  32018  dfon2lem6  32019  dfon2lem7  32020  dfon2lem8  32021  dfon2  32023  dford3lem1  38113  dford3lem2  38114
  Copyright terms: Public domain W3C validator