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

Theorem csbeq1d 3225
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 3222 . 2  |-  ( A  =  B  ->  [_ A  /  x ]_ C  = 
[_ B  /  x ]_ C )
31, 2syl 16 1  |-  ( ph  ->  [_ A  /  x ]_ C  =  [_ B  /  x ]_ C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649   [_csb 3219
This theorem is referenced by:  csbidmg  3272  csbco3g  3275  fmptcof  5869  mpt2mptsx  6381  dmmpt2ssx  6383  fmpt2x  6384  ovmptss  6395  fmpt2co  6397  xpf1o  7236  hsmexlem2  8271  iundom2g  8379  sumeq2ii  12450  summolem3  12471  summolem2a  12472  summo  12474  zsum  12475  fsum  12477  sumsn  12497  fsumcnv  12520  fsumcom2  12521  fsumshftm  12527  fsum0diag2  12529  ruclem1  12793  pcmpt  13224  gsumvalx  14737  odfval  15134  odval  15135  psrval  16392  psrass1lem  16405  fsum2cn  18862  iunmbl2  19412  dvfsumlem1  19871  itgsubst  19894  mpfrcl  19900  evlsval  19901  q1pval  20037  r1pval  20040  rlimcnp2  20766  fsumdvdscom  20931  fsumdvdsmul  20941  prodeq2ii  25200  prodmolem3  25220  prodmolem2a  25221  prodmo  25223  zprod  25224  fprod  25228  prodsn  25247  fprodcnv  25268  fprodcom2  25269  bpolylem  26006  bpolyval  26007  monotuz  26902  oddcomabszz  26905  fnwe2val  27022  fnwe2lem1  27023  fnwe2lem2  27024  mendval  27367  sumsnd  27572  cdleme31snd  30880  cdlemeg46c  31007  cdlemkid2  31418  cdlemk46  31442  cdlemk53b  31450  cdlemk53  31451
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-sbc 3130  df-csb 3220
  Copyright terms: Public domain W3C validator