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

Theorem csbeq1d 3427
Description: Equality deduction for proper substitution into a class. (Contributed by NM, 3-Dec-2005.)
Hypothesis
Ref Expression
csbeq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
csbeq1d  |-  ( ph  ->  [_ A  /  x ]_ C  =  [_ B  /  x ]_ C )

Proof of Theorem csbeq1d
StepHypRef Expression
1 csbeq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 csbeq1 3423 . 2  |-  ( A  =  B  ->  [_ A  /  x ]_ C  = 
[_ B  /  x ]_ C )
31, 2syl 16 1  |-  ( ph  ->  [_ A  /  x ]_ C  =  [_ B  /  x ]_ C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383   [_csb 3420
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-sbc 3314  df-csb 3421
This theorem is referenced by:  csbco3g  3830  csbidm  3832  csbidmgOLD  3833  fmptcof  6050  mpt2mptsx  6848  dmmpt2ssx  6850  fmpt2x  6851  ovmptss  6866  fmpt2co  6868  xpf1o  7681  cantnffvalOLD  8085  hsmexlem2  8810  iundom2g  8918  sumeq2ii  13497  summolem3  13518  summolem2a  13519  summo  13521  zsum  13522  fsum  13524  sumsn  13545  fsumcnv  13570  fsumcom2  13571  fsumshftm  13578  fsum0diag2  13580  prodeq2ii  13702  prodmolem3  13722  prodmolem2a  13723  prodmo  13725  zprod  13726  fprod  13730  prodsn  13749  fprodcnv  13769  fprodcom2  13770  ruclem1  13946  pcmpt  14393  gsumvalx  15876  odfval  16536  odval  16537  telgsumfzslem  16996  telgsumfzs  16997  psrval  17990  psrass1lem  18008  mpfrcl  18166  evlsval  18167  evls1fval  18335  fsum2cn  21353  iunmbl2  21945  dvfsumlem1  22405  itgsubst  22428  q1pval  22532  r1pval  22535  rlimcnp2  23274  fsumdvdscom  23439  fsumdvdsmul  23449  ttgval  24156  gsummpt2co  27749  msrfval  28875  bpolylem  29786  bpolyval  29787  monotuz  30853  oddcomabszz  30856  fnwe2val  30971  fnwe2lem1  30972  fnwe2lem2  30973  mendval  31108  sumsnd  31355  sumsnf  31524  prodsnf  31541  rnghmval  32532  dmmpt2ssx2  32794  fsumshftdOLD  34558  cdleme31snd  35987  cdlemeg46c  36114  cdlemkid2  36525  cdlemk46  36549  cdlemk53b  36557  cdlemk53  36558
  Copyright terms: Public domain W3C validator