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

Theorem csbeq1d 3698
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 3694 . 2 (𝐴 = 𝐵𝐴 / 𝑥𝐶 = 𝐵 / 𝑥𝐶)
31, 2syl 17 1 (𝜑𝐴 / 𝑥𝐶 = 𝐵 / 𝑥𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1652  csb 3691
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-sbc 3597  df-csb 3692
This theorem is referenced by:  csbco3g  4161  csbidm  4163  fmptcof  6588  mpt2mptsx  7434  dmmpt2ssx  7436  fmpt2x  7437  ovmptss  7460  fmpt2co  7462  xpf1o  8329  hsmexlem2  9502  iundom2g  9615  sumeq2ii  14708  summolem3  14730  summolem2a  14731  summo  14733  zsum  14734  fsum  14736  sumsnf  14758  fsumcnv  14789  fsumcom2  14790  fsumshftm  14797  fsum0diag2  14799  prodeq2ii  14926  prodmolem3  14946  prodmolem2a  14947  prodmo  14949  zprod  14950  fprod  14954  prodsn  14975  prodsnf  14977  fprodcnv  14996  fprodcom2  14997  bpolylem  15061  bpolyval  15062  ruclem1  15242  pcmpt  15875  gsumvalx  17536  odfval  18216  odval  18217  telgsumfzslem  18652  telgsumfzs  18653  psrval  19636  psrass1lem  19651  mpfrcl  19791  evlsval  19792  evls1fval  19957  fsum2cn  22953  iunmbl2  23615  dvfsumlem1  24080  itgsubst  24103  q1pval  24204  r1pval  24207  rlimcnp2  24984  fsumdvdscom  25202  fsumdvdsmul  25212  ttgval  26046  fsumiunle  30024  msrfval  31882  poimirlem1  33834  poimirlem3  33836  poimirlem4  33837  poimirlem5  33838  poimirlem6  33839  poimirlem7  33840  poimirlem8  33841  poimirlem10  33843  poimirlem11  33844  poimirlem12  33845  poimirlem15  33848  poimirlem16  33849  poimirlem17  33850  poimirlem18  33851  poimirlem19  33852  poimirlem20  33853  poimirlem21  33854  poimirlem22  33855  poimirlem23  33856  poimirlem24  33857  poimirlem25  33858  poimirlem26  33859  poimirlem27  33860  poimirlem28  33861  cdleme31snd  36342  cdlemeg46c  36469  cdlemkid2  36880  cdlemk46  36904  cdlemk53b  36912  cdlemk53  36913  monotuz  38183  oddcomabszz  38186  fnwe2val  38296  fnwe2lem1  38297  fnwe2lem2  38298  mendval  38430  sumsnd  39837  climinf2mpt  40584  climinfmpt  40585  sge0f1o  41236  rnghmval  42560  dmmpt2ssx2  42784
  Copyright terms: Public domain W3C validator