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

Theorem csbeq1d 3259
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 3256 . 2  |-  ( A  =  B  ->  [_ A  /  x ]_ C  = 
[_ B  /  x ]_ C )
31, 2syl 16 1  |-  ( ph  ->  [_ A  /  x ]_ C  =  [_ B  /  x ]_ C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653   [_csb 3253
This theorem is referenced by:  csbidmg  3306  csbco3g  3309  fmptcof  5905  mpt2mptsx  6417  dmmpt2ssx  6419  fmpt2x  6420  ovmptss  6431  fmpt2co  6433  xpf1o  7272  hsmexlem2  8312  iundom2g  8420  sumeq2ii  12492  summolem3  12513  summolem2a  12514  summo  12516  zsum  12517  fsum  12519  sumsn  12539  fsumcnv  12562  fsumcom2  12563  fsumshftm  12569  fsum0diag2  12571  ruclem1  12835  pcmpt  13266  gsumvalx  14779  odfval  15176  odval  15177  psrval  16434  psrass1lem  16447  fsum2cn  18906  iunmbl2  19456  dvfsumlem1  19915  itgsubst  19938  mpfrcl  19944  evlsval  19945  q1pval  20081  r1pval  20084  rlimcnp2  20810  fsumdvdscom  20975  fsumdvdsmul  20985  prodeq2ii  25244  prodmolem3  25264  prodmolem2a  25265  prodmo  25267  zprod  25268  fprod  25272  prodsn  25291  fprodcnv  25312  fprodcom2  25313  bpolylem  26099  bpolyval  26100  monotuz  27017  oddcomabszz  27020  fnwe2val  27137  fnwe2lem1  27138  fnwe2lem2  27139  mendval  27481  sumsnd  27686  cdleme31snd  31256  cdlemeg46c  31383  cdlemkid2  31794  cdlemk46  31818  cdlemk53b  31826  cdlemk53  31827
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-sbc 3164  df-csb 3254
  Copyright terms: Public domain W3C validator