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

Theorem csbeq1d 3310
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 3306 . 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 1369   [_csb 3303
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-sbc 3202  df-csb 3304
This theorem is referenced by:  csbco3g  3711  csbidm  3713  csbidmgOLD  3714  fmptcof  5892  mpt2mptsx  6652  dmmpt2ssx  6654  fmpt2x  6655  ovmptss  6669  fmpt2co  6671  xpf1o  7488  cantnffvalOLD  7886  hsmexlem2  8611  iundom2g  8719  sumeq2ii  13185  summolem3  13206  summolem2a  13207  summo  13209  zsum  13210  fsum  13212  sumsn  13232  fsumcnv  13255  fsumcom2  13256  fsumshftm  13263  fsum0diag2  13265  ruclem1  13528  pcmpt  13969  gsumvalx  15517  odfval  16051  odval  16052  psrval  17444  psrass1lem  17462  mpfrcl  17619  evlsval  17620  evls1fval  17769  fsum2cn  20462  iunmbl2  21053  dvfsumlem1  21513  itgsubst  21536  q1pval  21640  r1pval  21643  rlimcnp2  22375  fsumdvdscom  22540  fsumdvdsmul  22550  ttgval  23136  prodeq2ii  27441  prodmolem3  27461  prodmolem2a  27462  prodmo  27464  zprod  27465  fprod  27469  prodsn  27488  fprodcnv  27509  fprodcom2  27510  bpolylem  28206  bpolyval  28207  monotuz  29301  oddcomabszz  29304  fnwe2val  29421  fnwe2lem1  29422  fnwe2lem2  29423  mendval  29559  sumsnd  29767  dmmpt2ssx2  30746  telescfzgsumlem  30828  telescfzgsum  30829  fsumshftdOLD  32622  cdleme31snd  34049  cdlemeg46c  34176  cdlemkid2  34587  cdlemk46  34611  cdlemk53b  34619  cdlemk53  34620
  Copyright terms: Public domain W3C validator