Theorem csbeq1a 3867

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 3866	. 2 ⊢ ⦋𝑥 / 𝑥⦌𝐵 = 𝐵
2		csbeq1 3856	. 2 ⊢ (𝑥 = 𝐴 → ⦋𝑥 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
3	1, 2	eqtr3id 2778	1 ⊢ (𝑥 = 𝐴 → 𝐵 = ⦋𝐴 / 𝑥⦌𝐵)

Syntax hints:   → wi 4   = wceq 1540  ⦋csb 3853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-sbc 3745  df-csb 3854

This theorem is referenced by:  csbhypf  3881  csbiebt  3882  cbvrabcsfw  3894  cbvralcsf  3895  cbvreucsf  3897  cbvrabcsf  3898  rspc2vd  3901  sbcnestgfw  4374  sbcnestgf  4379  csbun  4394  csbin  4395  csbdif  4477  csbif  4536  disjors  5078  invdisjrab  5082  disjxiun  5092  disjxun  5093  sbcbr123  5149  eusvnf  5334  reusv2lem4  5343  reusv2  5345  moop2  5449  iunopeqop  5468  pofun  5549  opeliunxp  5690  opeliun2xp  5691  elrnmpt1  5906  resmptf  5994  csbima12  6034  csbcog  6249  fvmpt2f  6935  fvmpts  6937  fvmptdf  6940  fvmpt2i  6944  fvmptex  6948  fmptco  7067  fmptcof  7068  fmptcos  7069  elabrex  7182  elabrexg  7183  fliftfuns  7255  riotaeqimp  7336  csbov123  7397  ovmpos  7501  fvmpopr2d  7515  ofmpteq  7640  csbopeq1a  7992  mpomptsx  8006  dmmpossx  8008  fmpox  8009  el2mpocsbcl  8025  offval22  8028  ovmptss  8033  fmpoco  8035  mpoxeldm  8151  mpocurryd  8209  mpocurryvald  8210  fvmpocurryd  8211  eqerlem  8667  qliftfuns  8738  mptelixpg  8869  boxcutc  8875  xpf1o  9063  iunfi  9252  wdom2d  9491  ixpiunwdom  9501  hsmexlem2  10340  ac6c4  10394  iundom2g  10453  seqof2  13985  rlimcld2  15503  sumeq2ii  15618  summolem3  15639  summolem2a  15640  zsum  15643  fsum  15645  sumss2  15651  fsumcvg2  15652  fsumclf  15663  fsumzcl2  15664  fsumsplitf  15667  sumsnf  15668  fsumsplit1  15670  sumsns  15675  fsummsnunz  15679  fsumsplitsnun  15680  fsum2dlem  15695  fsumcnv  15698  fsumcom2  15699  fsumshftm  15706  fsum0diag2  15708  fsum00  15723  fsumabs  15726  fsumrlim  15736  fsumo1  15737  o1fsum  15738  fsumiun  15746  infcvgaux1i  15782  prodeq2ii  15836  prodmolem3  15858  prodmolem2a  15859  zprod  15862  fprod  15866  fprodntriv  15867  prodss  15872  fprodser  15874  fprodcllemf  15883  prodsn  15887  prodsnf  15889  fprodm1s  15895  fprodp1s  15896  prodsns  15897  fprodabs  15899  fprodn0  15904  fprod2dlem  15905  fprodcnv  15908  fprodcom2  15909  fproddivf  15912  fprodsplitf  15913  fprodsplit1f  15915  fprodle  15921  fprodmodd  15922  fprodefsum  16020  sumeven  16316  sumodd  16317  pcmpt  16822  pcmptdvds  16824  natpropd  17904  fucpropd  17905  gsummpt1n0  19862  gsumcom2  19872  gsummptnn0fz  19883  dprd2d2  19943  psrass1lem  21857  mpfrcl  22008  coe1fzgsumdlem  22206  gsumply1eq  22212  evl1gsumdlem  22259  mdetralt2  22512  mdetunilem2  22516  madugsum  22546  fiuncmp  23307  ptcld  23516  ptcldmpt  23517  ptclsg  23518  elmptrab  23730  prdsdsf  24271  prdsxmet  24273  fsumcn  24777  fsum2cn  24778  ovolfiniun  25418  ovoliunlem3  25421  ovoliun  25422  ovoliun2  25423  ovoliunnul  25424  finiunmbl  25461  volfiniun  25464  iundisj  25465  iundisj2  25466  iunmbl  25470  iunmbl2  25474  itgss3  25732  itgfsum  25744  itgabs  25752  limciun  25811  dvmptfsum  25895  dvfsumle  25942  dvfsumleOLD  25943  dvfsumabs  25945  dvfsumlem1  25948  dvfsumlem2  25949  dvfsumlem2OLD  25950  dvfsumlem3  25951  dvfsumlem4  25952  dvfsumrlim  25954  dvfsumrlim2  25955  dvfsum2  25957  itgsubstlem  25971  itgsubst  25972  rlimcnp2  26892  fsumdvdscom  27111  fsumdvdsmul  27121  fsumdvdsmulOLD  27123  fsumvma  27140  dchrisumlema  27415  dchrisumlem2  27417  dchrisumlem3  27418  ifeqeqx  32504  iunxpssiun1  32530  disjorsf  32542  disjabrex  32544  disjabrexf  32545  iundisjf  32551  iundisj2f  32552  disjunsn  32556  suppss2f  32595  2ndresdju  32606  fmptdF  32613  fmptcof2  32614  acunirnmpt2f  32618  aciunf1lem  32619  funcnv4mpt  32626  f1od2  32677  iundisjfi  32752  iundisj2fi  32753  fsumiunle  32787  gsummpt2co  33014  gsumpart  33023  gsumvsca1  33178  gsumvsca2  33179  rmfsupp2  33188  esumpfinvalf  34042  esum2dlem  34058  esumiun  34060  fiunelros  34140  measiun  34184  voliune  34195  volfiniune  34196  sbcaltop  35954  weiunpo  36438  weiunso  36439  weiunfr  36440  weiunse  36441  bj-sbeqALT  36873  rdgssun  37351  finxpreclem2  37363  phpreu  37583  finixpnum  37584  ptrest  37598  poimirlem23  37622  poimirlem24  37623  poimirlem25  37624  poimirlem26  37625  poimirlem27  37626  poimirlem28  37627  mbfposadd  37646  itgabsnc  37668  ftc1cnnclem  37670  ftc2nc  37681  fsumshftd  38930  riotasv2s  38936  cdleme31sn  40359  cdleme31sn1  40360  cdleme31se2  40362  cdleme32fva  40416  cdleme42b  40457  hlhilset  41913  evl1gprodd  42090  idomnnzgmulnz  42106  deg1gprod  42113  fmpocos  42207  mzpsubst  42721  rabdiophlem2  42775  elnn0rabdioph  42776  dvdsrabdioph  42783  fphpd  42789  monotuz  42914  oddcomabszz  42917  aomclem6  43032  flcidc  43143  fsumcnf  44999  sumsnd  45004  fiiuncl  45043  eliin2f  45082  disjf1  45161  disjrnmpt2  45166  disjinfi  45170  fmptf  45217  fmptff  45247  iuneqfzuzlem  45314  supxrleubrnmptf  45431  fsummulc1f  45553  fsumnncl  45554  fsumf1of  45556  fsumiunss  45557  fsumreclf  45558  fsumlessf  45559  fsumsermpt  45561  fprodexp  45576  fprodabs2  45577  mccllem  45579  fprodcnlem  45581  fprodcn  45582  climsubmpt  45642  climeldmeqmpt  45650  climfveqmpt  45653  climfveqmpt3  45664  climeldmeqmpt3  45671  climinf2mpt  45696  climinfmpt  45697  limsupequzmptf  45713  fprodcncf  45882  dvmptmulf  45919  dvnmptdivc  45920  dvmptfprod  45927  iblsplitf  45952  fourierdlem86  46174  fourierdlem112  46200  sge0f1o  46364  sge0lempt  46392  sge0iunmptlemfi  46395  sge0iunmptlemre  46397  sge0iunmpt  46400  sge0ltfirpmpt2  46408  sge0isummpt2  46414  sge0xaddlem2  46416  sge0xadd  46417  meadjiun  46448  hoimbl2  46647  vonhoire  46654  vonn0ioo2  46672  vonn0icc2  46674  csbafv12g  47122  csbaovg  47165  csbafv212g  47204  fsummsndifre  47357  fsumsplitsndif  47358  fsummmodsndifre  47359  fsummmodsnunz  47360  dmmpossx2  48309