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

Theorem sbceq1d 3332
 Description: Equality theorem for class substitution. (Contributed by Mario Carneiro, 9-Feb-2017.) (Revised by NM, 30-Jun-2018.)
Hypothesis
Ref Expression
sbceq1d.1
Assertion
Ref Expression
sbceq1d

Proof of Theorem sbceq1d
StepHypRef Expression
1 sbceq1d.1 . 2
2 dfsbcq 3329 . 2
31, 2syl 16 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  [.wsbc 3327 This theorem is referenced by:  sbceq1dd  3333  sbcnestgf  3839  ralrnmpt  6040  tfindes  6697  findes  6730  findcard2  7780  ac6sfi  7784  indexfi  7848  ac6num  8880  nn1suc  10582  uzind4s  11170  uzind4s2  11171  fzrevral  11792  fzshftral  11795  wrdind  12702  wrd2ind  12703  cjth  12936  prmind2  14228  isprs  15559  isdrs  15563  joinlem  15641  meetlem  15655  istos  15665  isdlat  15823  gsumvalx  15897  mrcmndind  15997  issrg  17159  islmod  17516  quotval  22688  nn0min  27611  sdclem2  30235  fdc  30238  rexrabdioph  30727  2nn0ind  30881  zindbi  30882  iotasbcq  31344  bnj944  33996  hdmap1ffval  37523  hdmap1fval  37524 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-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-cleq 2449  df-clel 2452  df-sbc 3328
 Copyright terms: Public domain W3C validator