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

Theorem csbeq1d 3441
Description: Equality deduction for proper substitution into a class. (Contributed by NM, 3-Dec-2005.)
Hypothesis
Ref Expression
csbeq1d.1
Assertion
Ref Expression
csbeq1d

Proof of Theorem csbeq1d
StepHypRef Expression
1 csbeq1d.1 . 2
2 csbeq1 3437 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  [_csb 3434
This theorem is referenced by:  csbco3g  3844  csbidm  3846  csbidmgOLD  3847  fmptcof  6065  mpt2mptsx  6863  dmmpt2ssx  6865  fmpt2x  6866  ovmptss  6881  fmpt2co  6883  xpf1o  7699  cantnffvalOLD  8103  hsmexlem2  8828  iundom2g  8936  sumeq2ii  13515  summolem3  13536  summolem2a  13537  summo  13539  zsum  13540  fsum  13542  sumsn  13563  fsumcnv  13588  fsumcom2  13589  fsumshftm  13596  fsum0diag2  13598  prodeq2ii  13720  prodmolem3  13740  prodmolem2a  13741  prodmo  13743  zprod  13744  fprod  13748  prodsn  13767  fprodcnv  13787  fprodcom2  13788  ruclem1  13964  pcmpt  14411  gsumvalx  15897  odfval  16557  odval  16558  telgsumfzslem  17017  telgsumfzs  17018  psrval  18011  psrass1lem  18029  mpfrcl  18187  evlsval  18188  evls1fval  18356  fsum2cn  21375  iunmbl2  21967  dvfsumlem1  22427  itgsubst  22450  q1pval  22554  r1pval  22557  rlimcnp2  23296  fsumdvdscom  23461  fsumdvdsmul  23471  ttgval  24178  gsummpt2co  27771  msrfval  28897  bpolylem  29810  bpolyval  29811  monotuz  30877  oddcomabszz  30880  fnwe2val  30995  fnwe2lem1  30996  fnwe2lem2  30997  mendval  31132  sumsnd  31401  sumsnf  31570  prodsnf  31587  rnghmval  32697  dmmpt2ssx2  32926  fsumshftdOLD  34683  cdleme31snd  36112  cdlemeg46c  36239  cdlemkid2  36650  cdlemk46  36674  cdlemk53b  36682  cdlemk53  36683
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-sbc 3328  df-csb 3435
  Copyright terms: Public domain W3C validator