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

Theorem treq 4680
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 4374 . . . 4 (𝐴 = 𝐵 𝐴 = 𝐵)
21sseq1d 3594 . . 3 (𝐴 = 𝐵 → ( 𝐴𝐴 𝐵𝐴))
3 sseq2 3589 . . 3 (𝐴 = 𝐵 → ( 𝐵𝐴 𝐵𝐵))
42, 3bitrd 266 . 2 (𝐴 = 𝐵 → ( 𝐴𝐴 𝐵𝐵))
5 df-tr 4675 . 2 (Tr 𝐴 𝐴𝐴)
6 df-tr 4675 . 2 (Tr 𝐵 𝐵𝐵)
74, 5, 63bitr4g 301 1 (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  wss 3539   cuni 4366  Tr wtr 4674
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rex 2901  df-in 3546  df-ss 3553  df-uni 4367  df-tr 4675
This theorem is referenced by:  truni  4689  ordeq  5633  trcl  8464  tz9.1  8465  tz9.1c  8466  tctr  8476  tcmin  8477  tc2  8478  r1tr  8499  r1elssi  8528  tcrank  8607  iswun  9382  tskr1om2  9446  elgrug  9470  grutsk  9500  dfon2lem1  30738  dfon2lem3  30740  dfon2lem4  30741  dfon2lem5  30742  dfon2lem6  30743  dfon2lem7  30744  dfon2lem8  30745  dfon2  30747  dford3lem1  36407  dford3lem2  36408
  Copyright terms: Public domain W3C validator