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

Theorem csbeq1d 3163
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 3160 . 2  |-  ( A  =  B  ->  [_ A  /  x ]_ C  = 
[_ B  /  x ]_ C )
31, 2syl 15 1  |-  ( ph  ->  [_ A  /  x ]_ C  =  [_ B  /  x ]_ C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1642   [_csb 3157
This theorem is referenced by:  csbidmg  3211  csbco3g  3214  fmptcof  5775  mpt2mptsx  6274  dmmpt2ssx  6276  fmpt2x  6277  ovmptss  6287  fmpt2co  6289  xpf1o  7111  hsmexlem2  8143  iundom2g  8252  sumeq2ii  12263  summolem3  12284  summolem2a  12285  summo  12287  zsum  12288  fsum  12290  sumsn  12310  fsumcnv  12333  fsumcom2  12334  fsumshftm  12340  fsum0diag2  12342  ruclem1  12606  pcmpt  13037  gsumvalx  14550  odfval  14947  odval  14948  psrval  16209  psrass1lem  16222  fsum2cn  18478  iunmbl2  19018  dvfsumlem1  19477  itgsubst  19500  mpfrcl  19506  evlsval  19507  q1pval  19643  r1pval  19646  rlimcnp2  20372  fsumdvdscom  20537  fsumdvdsmul  20547  prodeq2ii  24540  prodmolem3  24560  prodmolem2a  24561  prodmo  24563  zprod  24564  fprod  24568  prodsn  24587  bpolylem  25342  bpolyval  25343  monotuz  26349  oddcomabszz  26352  fnwe2val  26469  fnwe2lem1  26470  fnwe2lem2  26471  mendval  26814  sumsnd  27020  cdleme31snd  30644  cdlemeg46c  30771  cdlemkid2  31182  cdlemk46  31206  cdlemk53b  31214  cdlemk53  31215
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-sbc 3068  df-csb 3158
  Copyright terms: Public domain W3C validator