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

Theorem treq 5267
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 4918 . . . 4 (𝐴 = 𝐵 𝐴 = 𝐵)
21sseq1d 4015 . . 3 (𝐴 = 𝐵 → ( 𝐴𝐴 𝐵𝐴))
3 sseq2 4010 . . 3 (𝐴 = 𝐵 → ( 𝐵𝐴 𝐵𝐵))
42, 3bitrd 279 . 2 (𝐴 = 𝐵 → ( 𝐴𝐴 𝐵𝐵))
5 df-tr 5260 . 2 (Tr 𝐴 𝐴𝐴)
6 df-tr 5260 . 2 (Tr 𝐵 𝐵𝐵)
74, 5, 63bitr4g 314 1 (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206   = wceq 1540  wss 3951   cuni 4907  Tr wtr 5259
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-uni 4908  df-tr 5260
This theorem is referenced by:  truni  5275  trint  5277  ordeq  6391  trcl  9768  tz9.1  9769  tz9.1c  9770  tctr  9780  tcmin  9781  tc2  9782  r1tr  9816  r1elssi  9845  tcrank  9924  iswun  10744  tskr1om2  10808  elgrug  10832  grutsk  10862  dfon2lem1  35784  dfon2lem3  35786  dfon2lem4  35787  dfon2lem5  35788  dfon2lem6  35789  dfon2lem7  35790  dfon2lem8  35791  dfon2  35793  dford3lem1  43038  dford3lem2  43039  nadd1rabtr  43401  wfaxext  45010  wfaxrep  45011  wfaxpow  45014  wfaxinf2  45018  wfac8prim  45019
  Copyright terms: Public domain W3C validator