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

Theorem sbceq1a 3338
 Description: Equality theorem for class substitution. Class version of sbequ12 1992. (Contributed by NM, 26-Sep-2003.)
Assertion
Ref Expression
sbceq1a

Proof of Theorem sbceq1a
StepHypRef Expression
1 sbid 1996 . 2
2 dfsbcq2 3330 . 2
31, 2syl5bbr 259 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  [wsb 1739  [.wsbc 3327 This theorem is referenced by:  sbceq2a  3339  elrabsf  3366  cbvralcsf  3466  rabsnifsb  4098  euotd  4753  elfvmptrab1  5976  ralrnmpt  6040  riotass2  6284  riotass  6285  oprabv  6345  elovmpt2rab  6521  elovmpt2rab1  6522  ovmpt3rabdm  6535  elovmpt3rab1  6536  tfindes  6697  sbcopeq1a  6852  mpt2xopoveq  6966  findcard2  7780  ac6sfi  7784  indexfi  7848  uzindOLD  10982  nn0ind-raph  10989  fzrevral  11792  wrdind  12702  wrd2ind  12703  prmind2  14228  elmptrab  20328  isfildlem  20358  ifeqeqx  27419  setinds  29210  dfon2lem1  29215  tfisg  29284  wfisg  29289  frinsg  29325  indexdom  30225  sdclem2  30235  sdclem1  30236  fdc1  30239  sbccomieg  30726  rexrabdioph  30727  rexfrabdioph  30728  aomclem6  31005  pm13.13a  31314  pm13.13b  31315  pm13.14  31316  tratrb  33307  bnj919  33825  bnj976  33836  bnj1468  33904  bnj110  33916  bnj150  33934  bnj151  33935  bnj607  33974  bnj873  33982  bnj849  33983  bnj1388  34089  riotasv2s  34689 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-12 1854  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-sbc 3328
 Copyright terms: Public domain W3C validator