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

Theorem csbeq1d 3087
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 3084 . 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 1623   [_csb 3081
This theorem is referenced by:  csbidmg  3135  csbco3g  3138  fmptcof  5692  mpt2mptsx  6187  dmmpt2ssx  6189  fmpt2x  6190  ovmptss  6200  fmpt2co  6202  xpf1o  7023  hsmexlem2  8053  iundom2g  8162  sumeq2ii  12166  summolem3  12187  summolem2a  12188  summo  12190  zsum  12191  fsum  12193  sumsn  12213  fsumcnv  12236  fsumcom2  12237  fsumshftm  12243  fsum0diag2  12245  ruclem1  12509  pcmpt  12940  gsumvalx  14451  odfval  14848  odval  14849  psrval  16110  psrass1lem  16123  fsum2cn  18375  iunmbl2  18914  dvfsumlem1  19373  itgsubst  19396  mpfrcl  19402  evlsval  19403  q1pval  19539  r1pval  19542  rlimcnp2  20261  fsumdvdscom  20425  fsumdvdsmul  20435  bpolylem  24783  bpolyval  24784  monotuz  27026  oddcomabszz  27029  fnwe2val  27146  fnwe2lem1  27147  fnwe2lem2  27148  mendval  27491  sumsnd  27697  cdleme31snd  30575  cdlemeg46c  30702  cdlemkid2  31113  cdlemk46  31137  cdlemk53b  31145  cdlemk53  31146
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-sbc 2992  df-csb 3082
  Copyright terms: Public domain W3C validator