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

Theorem csbeq1d 3835
Description: Equality deduction for proper substitution into a class. (Contributed by NM, 3-Dec-2005.)
Hypothesis
Ref Expression
csbeq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
csbeq1d (𝜑𝐴 / 𝑥𝐶 = 𝐵 / 𝑥𝐶)

Proof of Theorem csbeq1d
StepHypRef Expression
1 csbeq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 csbeq1 3834 . 2 (𝐴 = 𝐵𝐴 / 𝑥𝐶 = 𝐵 / 𝑥𝐶)
31, 2syl 17 1 (𝜑𝐴 / 𝑥𝐶 = 𝐵 / 𝑥𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  csb 3831
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-sbc 3724  df-csb 3832
This theorem is referenced by:  csbeq12dv  3840  csbco3g  4339  csbidm  4341  fmptcof  6873  mpomptsx  7748  dmmpossx  7750  fmpox  7751  ovmptss  7775  fmpoco  7777  xpf1o  8667  hsmexlem2  9842  iundom2g  9955  sumeq2ii  15046  summolem3  15067  summolem2a  15068  summo  15070  zsum  15071  fsum  15073  sumsnf  15095  fsumcnv  15124  fsumcom2  15125  fsumshftm  15132  fsum0diag2  15134  prodeq2ii  15263  prodmolem3  15283  prodmolem2a  15284  prodmo  15286  zprod  15287  fprod  15291  prodsn  15312  prodsnf  15314  fprodcnv  15333  fprodcom2  15334  bpolylem  15398  bpolyval  15399  ruclem1  15580  pcmpt  16222  gsumvalx  17882  odfval  18656  odfvalALT  18657  odval  18658  telgsumfzslem  19105  telgsumfzs  19106  psrval  20604  psrass1lem  20619  mpfrcl  20761  evlsval  20762  evls1fval  20947  fsum2cn  23480  iunmbl2  24165  dvfsumlem1  24633  itgsubst  24656  q1pval  24758  r1pval  24761  rlimcnp2  25556  fsumdvdscom  25774  fsumdvdsmul  25784  ttgval  26673  fsumiunle  30575  msrfval  32898  poimirlem1  35057  poimirlem3  35059  poimirlem4  35060  poimirlem5  35061  poimirlem6  35062  poimirlem7  35063  poimirlem8  35064  poimirlem10  35066  poimirlem11  35067  poimirlem12  35068  poimirlem15  35071  poimirlem16  35072  poimirlem17  35073  poimirlem18  35074  poimirlem19  35075  poimirlem20  35076  poimirlem21  35077  poimirlem22  35078  poimirlem23  35079  poimirlem24  35080  poimirlem25  35081  poimirlem26  35082  poimirlem27  35083  poimirlem28  35084  cdleme31snd  37681  cdlemeg46c  37808  cdlemkid2  38219  cdlemk46  38243  cdlemk53b  38251  cdlemk53  38252  monotuz  39875  oddcomabszz  39878  fnwe2val  39986  fnwe2lem1  39987  fnwe2lem2  39988  mendval  40120  sumsnd  41648  climinf2mpt  42349  climinfmpt  42350  sge0f1o  43014  rnghmval  44508  dmmpossx2  44731
  Copyright terms: Public domain W3C validator