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

Theorem csbeq1d 3355
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 3351 . 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 1399   [_csb 3348
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-sbc 3253  df-csb 3349
This theorem is referenced by:  csbco3g  3767  csbidm  3769  fmptcof  5967  mpt2mptsx  6762  dmmpt2ssx  6764  fmpt2x  6765  ovmptss  6780  fmpt2co  6782  xpf1o  7598  cantnffvalOLD  7995  hsmexlem2  8720  iundom2g  8828  sumeq2ii  13517  summolem3  13538  summolem2a  13539  summo  13541  zsum  13542  fsum  13544  sumsn  13565  fsumcnv  13590  fsumcom2  13591  fsumshftm  13598  fsum0diag2  13600  prodeq2ii  13722  prodmolem3  13742  prodmolem2a  13743  prodmo  13745  zprod  13746  fprod  13750  prodsn  13769  fprodcnv  13789  fprodcom2  13790  ruclem1  13966  pcmpt  14413  gsumvalx  16014  odfval  16674  odval  16675  telgsumfzslem  17130  telgsumfzs  17131  psrval  18124  psrass1lem  18142  mpfrcl  18300  evlsval  18301  evls1fval  18469  fsum2cn  21460  iunmbl2  22052  dvfsumlem1  22512  itgsubst  22535  q1pval  22639  r1pval  22642  rlimcnp2  23413  fsumdvdscom  23578  fsumdvdsmul  23588  ttgval  24299  msrfval  29086  bpolylem  29963  bpolyval  29964  monotuz  31042  oddcomabszz  31045  fnwe2val  31161  fnwe2lem1  31162  fnwe2lem2  31163  mendval  31300  sumsnd  31568  sumsnf  31736  prodsnf  31753  rnghmval  32897  dmmpt2ssx2  33126  fsumshftdOLD  35096  cdleme31snd  36525  cdlemeg46c  36652  cdlemkid2  37063  cdlemk46  37087  cdlemk53b  37095  cdlemk53  37096
  Copyright terms: Public domain W3C validator