Theorem csbeq1a 3847

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

Syntax hints:   → wi 4   = wceq 1542  ⦋csb 3833

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-12 2184  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-sbc 3726  df-csb 3834

This theorem is referenced by:  csbhypf  3861  csbiebt  3862  cbvrabcsfw  3874  cbvralcsf  3875  cbvreucsf  3877  cbvrabcsf  3878  rspc2vd  3881  sbcnestgfw  4351  sbcnestgf  4356  csbun  4371  csbin  4372  csbdif  4455  csbif  4514  disjors  5057  invdisjrab  5061  disjxiun  5071  disjxun  5072  sbcbr123  5128  eusvnf  5323  reusv2lem4  5332  reusv2  5334  moop2  5445  iunopeqop  5464  iunopeqopOLD  5465  pofun  5546  opeliunxp  5687  opeliun2xp  5688  elrnmpt1  5904  resmptf  5993  csbima12  6033  csbcog  6250  fvmpt2f  6937  fvmpts  6940  fvmptdf  6943  fvmpt2i  6947  fvmptex  6951  fmptco  7071  fmptcof  7072  fmptcos  7073  elabrex  7186  elabrexg  7187  fliftfuns  7258  riotaeqimp  7339  csbov123  7400  ovmpos  7504  fvmpopr2d  7518  ofmpteq  7643  csbopeq1a  7992  mpomptsx  8006  dmmpossx  8008  fmpox  8009  el2mpocsbcl  8024  offval22  8027  ovmptss  8032  fmpoco  8034  mpoxeldm  8150  mpocurryd  8208  mpocurryvald  8209  fvmpocurryd  8210  eqerlem  8668  qliftfuns  8740  mptelixpg  8872  boxcutc  8878  xpf1o  9066  iunfi  9242  wdom2d  9484  ixpiunwdom  9494  hsmexlem2  10338  ac6c4  10392  iundom2g  10451  seqof2  14011  rlimcld2  15529  sumeq2ii  15644  summolem3  15665  summolem2a  15666  zsum  15669  fsum  15671  sumss2  15677  fsumcvg2  15678  fsumclf  15689  fsumzcl2  15690  fsumsplitf  15693  sumsnf  15694  fsumsplit1  15696  sumsns  15701  fsummsnunz  15705  fsumsplitsnun  15706  fsum2dlem  15721  fsumcnv  15724  fsumcom2  15725  fsumshftm  15732  fsum0diag2  15734  fsum00  15750  fsumabs  15753  fsumrlim  15763  fsumo1  15764  o1fsum  15765  fsumiun  15773  infcvgaux1i  15811  prodeq2ii  15865  prodmolem3  15887  prodmolem2a  15888  zprod  15891  fprod  15895  fprodntriv  15896  prodss  15901  fprodser  15903  fprodcllemf  15912  prodsn  15916  prodsnf  15918  fprodm1s  15924  fprodp1s  15925  prodsns  15926  fprodabs  15928  fprodn0  15933  fprod2dlem  15934  fprodcnv  15937  fprodcom2  15938  fproddivf  15941  fprodsplitf  15942  fprodsplit1f  15944  fprodle  15950  fprodmodd  15951  fprodefsum  16049  sumeven  16345  sumodd  16346  pcmpt  16852  pcmptdvds  16854  natpropd  17935  fucpropd  17936  gsummpt1n0  19929  gsumcom2  19939  gsummptnn0fz  19950  dprd2d2  20010  psrass1lem  21901  mpfrcl  22052  coe1fzgsumdlem  22256  gsumply1eq  22262  evl1gsumdlem  22309  mdetralt2  22562  mdetunilem2  22566  madugsum  22596  fiuncmp  23357  ptcld  23566  ptcldmpt  23567  ptclsg  23568  elmptrab  23780  prdsdsf  24320  prdsxmet  24322  fsumcn  24825  fsum2cn  24826  ovolfiniun  25456  ovoliunlem3  25459  ovoliun  25460  ovoliun2  25461  ovoliunnul  25462  finiunmbl  25499  volfiniun  25502  iundisj  25503  iundisj2  25504  iunmbl  25508  iunmbl2  25512  itgss3  25770  itgfsum  25782  itgabs  25790  limciun  25849  dvmptfsum  25930  dvfsumle  25976  dvfsumabs  25978  dvfsumlem1  25981  dvfsumlem2  25982  dvfsumlem3  25983  dvfsumlem4  25984  dvfsumrlim  25986  dvfsumrlim2  25987  dvfsum2  25989  itgsubstlem  26003  itgsubst  26004  rlimcnp2  26918  fsumdvdscom  27136  fsumdvdsmul  27146  fsumvma  27164  dchrisumlema  27439  dchrisumlem2  27441  dchrisumlem3  27442  ifeqeqx  32600  iunxpssiun1  32626  disjorsf  32638  disjabrex  32640  disjabrexf  32641  iundisjf  32647  iundisj2f  32648  disjunsn  32652  suppss2f  32699  2ndresdju  32710  fmptdF  32717  fmptcof2  32718  acunirnmpt2f  32722  aciunf1lem  32723  funcnv4mpt  32729  f1od2  32780  iundisjfi  32857  iundisj2fi  32858  fsumiunle  32890  gsummpt2co  33097  gsummptp1  33106  gsumpart  33112  gsumvsca1  33275  gsumvsca2  33276  rmfsupp2  33287  esumpfinvalf  34208  esum2dlem  34224  esumiun  34226  fiunelros  34306  measiun  34350  voliune  34361  volfiniune  34362  sbcaltop  36151  weiunpo  36635  weiunso  36636  weiunfr  36637  weiunse  36638  csbttc  36679  bj-sbeqALT  37195  rdgssun  37682  finxpreclem2  37694  phpreu  37913  finixpnum  37914  ptrest  37928  poimirlem23  37952  poimirlem24  37953  poimirlem25  37954  poimirlem26  37955  poimirlem27  37956  poimirlem28  37957  mbfposadd  37976  itgabsnc  37998  ftc1cnnclem  38000  ftc2nc  38011  fsumshftd  39386  riotasv2s  39392  cdleme31sn  40814  cdleme31sn1  40815  cdleme31se2  40817  cdleme32fva  40871  cdleme42b  40912  hlhilset  42368  evl1gprodd  42544  idomnnzgmulnz  42560  deg1gprod  42567  fmpocos  42663  mzpsubst  43168  rabdiophlem2  43218  elnn0rabdioph  43219  dvdsrabdioph  43226  fphpd  43232  monotuz  43357  oddcomabszz  43360  aomclem6  43475  flcidc  43586  fsumcnf  45440  sumsnd  45445  fiiuncl  45484  eliin2f  45522  disjf1  45601  disjrnmpt2  45606  disjinfi  45610  fmptf  45656  fmptff  45686  iuneqfzuzlem  45752  supxrleubrnmptf  45867  fsummulc1f  45989  fsumnncl  45990  fsumf1of  45992  fsumiunss  45993  fsumreclf  45994  fsumlessf  45995  fsumsermpt  45997  fprodexp  46012  fprodabs2  46013  mccllem  46015  fprodcnlem  46017  fprodcn  46018  climsubmpt  46076  climeldmeqmpt  46084  climfveqmpt  46087  climfveqmpt3  46098  climeldmeqmpt3  46105  climinf2mpt  46130  climinfmpt  46131  limsupequzmptf  46147  fprodcncf  46316  dvmptmulf  46353  dvnmptdivc  46354  dvmptfprod  46361  iblsplitf  46386  fourierdlem86  46608  fourierdlem112  46634  sge0f1o  46798  sge0lempt  46826  sge0iunmptlemfi  46829  sge0iunmptlemre  46831  sge0iunmpt  46834  sge0ltfirpmpt2  46842  sge0isummpt2  46848  sge0xaddlem2  46850  sge0xadd  46851  meadjiun  46882  hoimbl2  47081  vonhoire  47088  vonn0ioo2  47106  vonn0icc2  47108  csbafv12g  47573  csbaovg  47616  csbafv212g  47655  fsummsndifre  47816  fsumsplitsndif  47817  fsummmodsndifre  47818  fsummmodsnunz  47819  dmmpossx2  48801