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

Theorem csbeq1d 3217
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 3214 . 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 3211
This theorem is referenced by:  csbidmg  3264  csbco3g  3267  fmptcof  5861  mpt2mptsx  6373  dmmpt2ssx  6375  fmpt2x  6376  ovmptss  6387  fmpt2co  6389  xpf1o  7228  hsmexlem2  8263  iundom2g  8371  sumeq2ii  12442  summolem3  12463  summolem2a  12464  summo  12466  zsum  12467  fsum  12469  sumsn  12489  fsumcnv  12512  fsumcom2  12513  fsumshftm  12519  fsum0diag2  12521  ruclem1  12785  pcmpt  13216  gsumvalx  14729  odfval  15126  odval  15127  psrval  16384  psrass1lem  16397  fsum2cn  18854  iunmbl2  19404  dvfsumlem1  19863  itgsubst  19886  mpfrcl  19892  evlsval  19893  q1pval  20029  r1pval  20032  rlimcnp2  20758  fsumdvdscom  20923  fsumdvdsmul  20933  prodeq2ii  25192  prodmolem3  25212  prodmolem2a  25213  prodmo  25215  zprod  25216  fprod  25220  prodsn  25239  fprodcnv  25260  fprodcom2  25261  bpolylem  25998  bpolyval  25999  monotuz  26894  oddcomabszz  26897  fnwe2val  27014  fnwe2lem1  27015  fnwe2lem2  27016  mendval  27359  sumsnd  27564  cdleme31snd  30868  cdlemeg46c  30995  cdlemkid2  31406  cdlemk46  31430  cdlemk53b  31438  cdlemk53  31439
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 2385
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 2391  df-cleq 2397  df-clel 2400  df-sbc 3122  df-csb 3212
  Copyright terms: Public domain W3C validator