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

Theorem csbeq1d 3292
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 3288 . 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 1364   [_csb 3285
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-sbc 3184  df-csb 3286
This theorem is referenced by:  csbco3g  3693  csbidm  3695  csbidmgOLD  3696  fmptcof  5874  mpt2mptsx  6636  dmmpt2ssx  6638  fmpt2x  6639  ovmptss  6653  fmpt2co  6655  xpf1o  7469  cantnffvalOLD  7867  hsmexlem2  8592  iundom2g  8700  sumeq2ii  13166  summolem3  13187  summolem2a  13188  summo  13190  zsum  13191  fsum  13193  sumsn  13213  fsumcnv  13236  fsumcom2  13237  fsumshftm  13244  fsum0diag2  13246  ruclem1  13509  pcmpt  13950  gsumvalx  15497  odfval  16029  odval  16030  psrval  17407  psrass1lem  17425  mpfrcl  17580  evlsval  17581  evls1fval  17727  fsum2cn  20406  iunmbl2  20997  dvfsumlem1  21457  itgsubst  21480  q1pval  21584  r1pval  21587  rlimcnp2  22319  fsumdvdscom  22484  fsumdvdsmul  22494  ttgval  23056  prodeq2ii  27355  prodmolem3  27375  prodmolem2a  27376  prodmo  27378  zprod  27379  fprod  27383  prodsn  27402  fprodcnv  27423  fprodcom2  27424  bpolylem  28120  bpolyval  28121  monotuz  29207  oddcomabszz  29210  fnwe2val  29327  fnwe2lem1  29328  fnwe2lem2  29329  mendval  29465  sumsnd  29673  dmmpt2ssx2  30651  cdleme31snd  33752  cdlemeg46c  33879  cdlemkid2  34290  cdlemk46  34314  cdlemk53b  34322  cdlemk53  34323
  Copyright terms: Public domain W3C validator