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

Theorem treq 4551
Description: Equality theorem for the transitive class predicate. (Contributed by NM, 17-Sep-1993.)
Assertion
Ref Expression
treq

Proof of Theorem treq
StepHypRef Expression
1 unieq 4257 . . . 4
21sseq1d 3530 . . 3
3 sseq2 3525 . . 3
42, 3bitrd 253 . 2
5 df-tr 4546 . 2
6 df-tr 4546 . 2
74, 5, 63bitr4g 288 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  C_wss 3475  U.cuni 4249  Trwtr 4545
This theorem is referenced by:  truni  4559  ordeq  4890  trcl  8180  tz9.1  8181  tz9.1c  8182  tctr  8192  tcmin  8193  tc2  8194  r1tr  8215  r1elssi  8244  tcrank  8323  iswun  9103  tskr1om2  9167  elgrug  9191  grutsk  9221  dfon2lem1  29215  dfon2lem3  29217  dfon2lem4  29218  dfon2lem5  29219  dfon2lem6  29220  dfon2lem7  29221  dfon2lem8  29222  dfon2  29224  dford3lem1  30968  dford3lem2  30969
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813  df-in 3482  df-ss 3489  df-uni 4250  df-tr 4546
  Copyright terms: Public domain W3C validator