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

Theorem csbeq1d 3442
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 3438 . 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 1379   [_csb 3435
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-sbc 3332  df-csb 3436
This theorem is referenced by:  csbco3g  3844  csbidm  3846  csbidmgOLD  3847  fmptcof  6053  mpt2mptsx  6844  dmmpt2ssx  6846  fmpt2x  6847  ovmptss  6861  fmpt2co  6863  xpf1o  7676  cantnffvalOLD  8078  hsmexlem2  8803  iundom2g  8911  sumeq2ii  13474  summolem3  13495  summolem2a  13496  summo  13498  zsum  13499  fsum  13501  sumsn  13522  fsumcnv  13547  fsumcom2  13548  fsumshftm  13555  fsum0diag2  13557  ruclem1  13821  pcmpt  14266  gsumvalx  15815  odfval  16353  odval  16354  telgsumfzslem  16808  telgsumfzs  16809  psrval  17782  psrass1lem  17800  mpfrcl  17958  evlsval  17959  evls1fval  18127  fsum2cn  21110  iunmbl2  21702  dvfsumlem1  22162  itgsubst  22185  q1pval  22289  r1pval  22292  rlimcnp2  23024  fsumdvdscom  23189  fsumdvdsmul  23199  ttgval  23854  prodeq2ii  28622  prodmolem3  28642  prodmolem2a  28643  prodmo  28645  zprod  28646  fprod  28650  prodsn  28669  fprodcnv  28690  fprodcom2  28691  bpolylem  29387  bpolyval  29388  monotuz  30481  oddcomabszz  30484  fnwe2val  30599  fnwe2lem1  30600  fnwe2lem2  30601  mendval  30737  sumsnd  30979  dmmpt2ssx2  31990  fsumshftdOLD  33755  cdleme31snd  35182  cdlemeg46c  35309  cdlemkid2  35720  cdlemk46  35744  cdlemk53b  35752  cdlemk53  35753
  Copyright terms: Public domain W3C validator