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

Theorem treq 4791
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 4476 . . . 4 (𝐴 = 𝐵 𝐴 = 𝐵)
21sseq1d 3665 . . 3 (𝐴 = 𝐵 → ( 𝐴𝐴 𝐵𝐴))
3 sseq2 3660 . . 3 (𝐴 = 𝐵 → ( 𝐵𝐴 𝐵𝐵))
42, 3bitrd 268 . 2 (𝐴 = 𝐵 → ( 𝐴𝐴 𝐵𝐵))
5 df-tr 4786 . 2 (Tr 𝐴 𝐴𝐴)
6 df-tr 4786 . 2 (Tr 𝐵 𝐵𝐵)
74, 5, 63bitr4g 303 1 (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1523  wss 3607   cuni 4468  Tr wtr 4785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rex 2947  df-in 3614  df-ss 3621  df-uni 4469  df-tr 4786
This theorem is referenced by:  truni  4800  ordeq  5768  trcl  8642  tz9.1  8643  tz9.1c  8644  tctr  8654  tcmin  8655  tc2  8656  r1tr  8677  r1elssi  8706  tcrank  8785  iswun  9564  tskr1om2  9628  elgrug  9652  grutsk  9682  dfon2lem1  31812  dfon2lem3  31814  dfon2lem4  31815  dfon2lem5  31816  dfon2lem6  31817  dfon2lem7  31818  dfon2lem8  31819  dfon2  31821  dford3lem1  37910  dford3lem2  37911
  Copyright terms: Public domain W3C validator