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

Theorem csbeq1d 3345
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 3341 . 2  |-  ( A  =  B  ->  [_ A  /  x ]_ C  = 
[_ B  /  x ]_ C )
31, 2syl 17 1  |-  ( ph  ->  [_ A  /  x ]_ C  =  [_ B  /  x ]_ C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437   [_csb 3338
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-sbc 3243  df-csb 3339
This theorem is referenced by:  csbco3g  3762  csbidm  3764  fmptcof  6016  mpt2mptsx  6814  dmmpt2ssx  6816  fmpt2x  6817  ovmptss  6832  fmpt2co  6834  xpf1o  7687  hsmexlem2  8808  iundom2g  8916  sumeq2ii  13702  summolem3  13723  summolem2a  13724  summo  13726  zsum  13727  fsum  13729  sumsn  13750  fsumcnv  13777  fsumcom2  13778  fsumshftm  13785  fsum0diag2  13787  prodeq2ii  13910  prodmolem3  13930  prodmolem2a  13931  prodmo  13933  zprod  13934  fprod  13938  prodsn  13959  prodsnf  13961  fprodcnv  13980  fprodcom2  13981  bpolylem  14044  bpolyval  14045  ruclem1  14226  pcmpt  14780  gsumvalx  16456  odfval  17122  odval  17123  odfvalOLD  17125  odvalOLD  17126  telgsumfzslem  17561  telgsumfzs  17562  psrval  18529  psrass1lem  18544  mpfrcl  18684  evlsval  18685  evls1fval  18851  fsum2cn  21845  iunmbl2  22452  dvfsumlem1  22920  itgsubst  22943  q1pval  23046  r1pval  23049  rlimcnp2  23834  fsumdvdscom  24056  fsumdvdsmul  24066  ttgval  24847  msrfval  30127  poimirlem1  31848  poimirlem3  31850  poimirlem4  31851  poimirlem5  31852  poimirlem6  31853  poimirlem7  31854  poimirlem8  31855  poimirlem10  31857  poimirlem11  31858  poimirlem12  31859  poimirlem15  31862  poimirlem16  31863  poimirlem17  31864  poimirlem18  31865  poimirlem19  31866  poimirlem20  31867  poimirlem21  31868  poimirlem22  31869  poimirlem23  31870  poimirlem24  31871  poimirlem25  31872  poimirlem26  31873  poimirlem27  31874  poimirlem28  31875  fsumshftdOLD  32436  cdleme31snd  33865  cdlemeg46c  33992  cdlemkid2  34403  cdlemk46  34427  cdlemk53b  34435  cdlemk53  34436  monotuz  35702  oddcomabszz  35705  fnwe2val  35820  fnwe2lem1  35821  fnwe2lem2  35822  mendval  35962  sumsnd  37263  sumsnf  37532  sge0f1o  38075  rnghmval  39492  dmmpt2ssx2  39721
  Copyright terms: Public domain W3C validator