Theorem csbeq1a 3857

Description: Equality theorem for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)

Assertion

Ref	Expression
csbeq1a	⊢ (𝑥 = 𝐴 → 𝐵 = ⦋𝐴 / 𝑥⦌𝐵)

Proof of Theorem csbeq1a

Step	Hyp	Ref	Expression
1		csbid 3856	. 2 ⊢ ⦋𝑥 / 𝑥⦌𝐵 = 𝐵
2		csbeq1 3846	. 2 ⊢ (𝑥 = 𝐴 → ⦋𝑥 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
3	1, 2	eqtr3id 2801	1 ⊢ (𝑥 = 𝐴 → 𝐵 = ⦋𝐴 / 𝑥⦌𝐵)

Syntax hints:   → wi 4   = wceq 1550  ⦋csb 3843

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-12 2202  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1553  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-sbc 3736  df-csb 3844

This theorem is referenced by:  csbhypf  3871  csbiebt  3872  cbvrabcsfw  3884  cbvralcsf  3885  cbvreucsf  3887  cbvrabcsf  3888  rspc2vd  3891  sbcnestgfw  4365  sbcnestgf  4370  csbun  4385  csbin  4386  csbdif  4469  csbif  4528  disjors  5073  invdisjrab  5077  disjxiun  5087  disjxun  5088  sbcbr123  5144  eusvnf  5339  reusv2lem4  5348  reusv2  5350  moop2  5461  iunopeqop  5480  iunopeqopOLD  5481  pofun  5562  opeliunxp  5703  opeliun2xp  5704  elrnmpt1  5925  resmptf  6014  csbima12  6054  csbcog  6269  fvmpt2f  6961  fvmpts  6964  fvmptdf  6967  fvmpt2i  6971  fvmptex  6975  fmptco  7096  fmptcof  7097  fmptcos  7098  elabrex  7211  elabrexg  7212  fliftfuns  7283  riotaeqimp  7364  csbov123  7425  ovmpos  7529  fvmpopr2d  7543  ofmpteq  7668  csbopeq1a  8016  mpomptsx  8030  dmmpossx  8032  fmpox  8033  el2mpocsbcl  8048  offval22  8051  ovmptss  8056  fmpoco  8058  mpoxeldm  8175  mpocurryd  8233  mpocurryvald  8234  fvmpocurryd  8235  eqerlem  8698  qliftfuns  8770  mptelixpg  8902  boxcutc  8908  xpf1o  9096  iunfi  9272  wdom2d  9514  ixpiunwdom  9524  hsmexlem2  10370  ac6c4  10424  iundom2g  10483  seqof2  14059  rlimcld2  15577  sumeq2ii  15692  summolem3  15713  summolem2a  15714  zsum  15717  fsum  15719  sumss2  15725  fsumcvg2  15726  fsumclf  15737  fsumzcl2  15738  fsumsplitf  15741  sumsnf  15742  fsumsplit1  15744  sumsns  15749  fsummsnunz  15753  fsumsplitsnun  15754  fsum2dlem  15769  fsumcnv  15772  fsumcom2  15773  fsumshftm  15780  fsum0diag2  15782  fsum00  15798  fsumabs  15801  fsumrlim  15811  fsumo1  15812  o1fsum  15813  fsumiun  15821  infcvgaux1i  15859  prodeq2ii  15913  prodmolem3  15935  prodmolem2a  15936  zprod  15939  fprod  15943  fprodntriv  15944  prodss  15949  fprodser  15951  fprodcllemf  15960  prodsn  15964  prodsnf  15966  fprodm1s  15972  fprodp1s  15973  prodsns  15974  fprodabs  15976  fprodn0  15981  fprod2dlem  15982  fprodcnv  15985  fprodcom2  15986  fproddivf  15989  fprodsplitf  15990  fprodsplit1f  15992  fprodle  15998  fprodmodd  15999  fprodefsum  16097  sumeven  16393  sumodd  16394  pcmpt  16900  pcmptdvds  16902  natpropd  17984  fucpropd  17985  gsummpt1n0  19977  gsumcom2  19987  gsummptnn0fz  19998  dprd2d2  20058  psrass1lem  21954  mpfrcl  22107  coe1fzgsumdlem  22335  gsumply1eq  22341  evl1gsumdlem  22388  mdetralt2  22638  mdetunilem2  22642  madugsum  22672  fiuncmp  23433  ptcld  23642  ptcldmpt  23643  ptclsg  23644  elmptrab  23856  prdsdsf  24396  prdsxmet  24398  fsumcn  24901  fsum2cn  24902  ovolfiniun  25532  ovoliunlem3  25535  ovoliun  25536  ovoliun2  25537  ovoliunnul  25538  finiunmbl  25575  volfiniun  25578  iundisj  25579  iundisj2  25580  iunmbl  25584  iunmbl2  25588  itgss3  25846  itgfsum  25858  itgabs  25866  limciun  25925  dvmptfsum  26006  dvfsumle  26052  dvfsumabs  26054  dvfsumlem1  26057  dvfsumlem2  26058  dvfsumlem3  26059  dvfsumlem4  26060  dvfsumrlim  26062  dvfsumrlim2  26063  dvfsum2  26065  itgsubstlem  26079  itgsubst  26080  rlimcnp2  26997  fsumdvdscom  27215  fsumdvdsmul  27225  fsumvma  27243  dchrisumlema  27518  dchrisumlem2  27520  dchrisumlem3  27521  ifeqeqx  32679  iunxpssiun1  32706  disjorsf  32718  disjabrex  32720  disjabrexf  32721  iundisjf  32727  iundisj2f  32728  disjunsn  32732  suppss2f  32779  2ndresdju  32790  fmptdF  32797  fmptcof2  32798  acunirnmpt2f  32802  aciunf1lem  32803  funcnv4mpt  32809  f1od2  32860  iundisjfi  32937  iundisj2fi  32938  fsumiunle  32970  gsummpt2co  33178  gsummptp1  33187  gsumpart  33193  gsumvsca1  33356  gsumvsca2  33357  rmfsupp2  33368  esumpfinvalf  34317  esum2dlem  34333  esumiun  34335  fiunelros  34415  measiun  34459  voliune  34470  volfiniune  34471  sbcaltop  36269  weiunpo  36763  weiunso  36764  weiunfr  36765  weiunse  36766  csbttc  36807  bj-sbeqALT  37323  rdgssun  37810  finxpreclem2  37822  phpreu  38041  finixpnum  38042  ptrest  38056  poimirlem23  38080  poimirlem24  38081  poimirlem25  38082  poimirlem26  38083  poimirlem27  38084  poimirlem28  38085  mbfposadd  38104  itgabsnc  38126  ftc1cnnclem  38128  ftc2nc  38139  fsumshftd  39514  riotasv2s  39520  cdleme31sn  40942  cdleme31sn1  40943  cdleme31se2  40945  cdleme32fva  40999  cdleme42b  41040  hlhilset  42496  evl1gprodd  42672  idomnnzgmulnz  42688  deg1gprod  42695  fmpocos  42790  mzpsubst  43267  rabdiophlem2  43317  elnn0rabdioph  43318  dvdsrabdioph  43325  fphpd  43331  monotuz  43456  oddcomabszz  43459  aomclem6  43574  flcidc  43685  fsumcnf  45539  sumsnd  45544  fiiuncl  45583  eliin2f  45620  disjf1  45699  disjrnmpt2  45704  disjinfi  45708  fmptf  45752  fmptff  45782  iuneqfzuzlem  45848  supxrleubrnmptf  45963  fsummulc1f  46085  fsumnncl  46086  fsumf1of  46088  fsumiunss  46089  fsumreclf  46090  fsumlessf  46091  fsumsermpt  46093  fprodexp  46108  fprodabs2  46109  mccllem  46111  fprodcnlem  46113  fprodcn  46114  climsubmpt  46172  climeldmeqmpt  46180  climfveqmpt  46183  climfveqmpt3  46194  climeldmeqmpt3  46201  climinf2mpt  46226  climinfmpt  46227  limsupequzmptf  46243  fprodcncf  46412  dvmptmulf  46449  dvnmptdivc  46450  dvmptfprod  46457  iblsplitf  46482  fourierdlem86  46704  fourierdlem112  46730  sge0f1o  46894  sge0lempt  46922  sge0iunmptlemfi  46925  sge0iunmptlemre  46927  sge0iunmpt  46930  sge0ltfirpmpt2  46938  sge0isummpt2  46944  sge0xaddlem2  46946  sge0xadd  46947  meadjiun  46978  hoimbl2  47177  vonhoire  47184  vonn0ioo2  47202  vonn0icc2  47204  csbafv12g  47669  csbaovg  47712  csbafv212g  47751  fsummsndifre  47912  fsumsplitsndif  47913  fsummmodsndifre  47914  fsummmodsnunz  47915  dmmpossx2  48897