Theorem csbeq1a 3825

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

Syntax hints:   → wi 4   = wceq 1543  ⦋csb 3811

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-12 2175  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-sbc 3695  df-csb 3812

This theorem is referenced by:  csbhypf  3840  csbiebt  3841  cbvrabcsfw  3855  cbvralcsf  3856  cbvreucsf  3858  cbvrabcsf  3859  rspc2vd  3862  sbcnestgfw  4333  sbcnestgf  4338  csbun  4353  csbin  4354  csbif  4496  disjors  5034  invdisjrabw  5038  invdisjrab  5039  disjxiun  5050  disjxun  5051  sbcbr123  5107  eusvnf  5285  reusv2lem4  5294  reusv2  5296  moop2  5385  iunopeqop  5404  pofun  5486  opeliunxp  5616  elrnmpt1  5827  resmptf  5907  csbima12  5947  fvmpt2f  6819  fvmpts  6821  fvmptdf  6824  fvmpt2i  6828  fvmptex  6832  fmptco  6944  fmptcof  6945  fmptcos  6946  elabrex  7056  fliftfuns  7123  riotaeqimp  7197  csbov123  7255  ovmpos  7357  fvmpopr2d  7370  ofmpteq  7490  csbopeq1a  7821  mpomptsx  7834  dmmpossx  7836  fmpox  7837  el2mpocsbcl  7853  offval22  7856  ovmptss  7861  fmpoco  7863  mpoxeldm  7953  mpocurryd  8011  mpocurryvald  8012  fvmpocurryd  8013  eqerlem  8425  qliftfuns  8486  mptelixpg  8616  boxcutc  8622  xpf1o  8808  iunfi  8964  wdom2d  9196  ixpiunwdom  9206  hsmexlem2  10041  ac6c4  10095  iundom2g  10154  seqof2  13634  rlimcld2  15139  sumeq2ii  15257  summolem3  15278  summolem2a  15279  zsum  15282  fsum  15284  sumss2  15290  fsumcvg2  15291  fsumclf  15302  fsumzcl2  15303  fsumsplitf  15306  sumsnf  15307  fsumsplit1  15309  sumsns  15314  fsummsnunz  15318  fsumsplitsnun  15319  fsum2dlem  15334  fsumcnv  15337  fsumcom2  15338  fsumshftm  15345  fsum0diag2  15347  fsum00  15362  fsumabs  15365  fsumrlim  15375  fsumo1  15376  o1fsum  15377  fsumiun  15385  infcvgaux1i  15421  prodeq2ii  15475  prodmolem3  15495  prodmolem2a  15496  zprod  15499  fprod  15503  fprodntriv  15504  prodss  15509  fprodser  15511  fprodcllemf  15520  prodsn  15524  prodsnf  15526  fprodm1s  15532  fprodp1s  15533  prodsns  15534  fprodabs  15536  fprodn0  15541  fprod2dlem  15542  fprodcnv  15545  fprodcom2  15546  fproddivf  15549  fprodsplitf  15550  fprodsplit1f  15552  fprodle  15558  fprodmodd  15559  fprodefsum  15656  sumeven  15948  sumodd  15949  pcmpt  16445  pcmptdvds  16447  natpropd  17485  fucpropd  17486  gsummpt1n0  19350  gsumcom2  19360  gsummptnn0fz  19371  dprd2d2  19431  psrass1lemOLD  20899  psrass1lem  20902  mpfrcl  21045  coe1fzgsumdlem  21222  gsumply1eq  21226  evl1gsumdlem  21272  mdetralt2  21506  mdetunilem2  21510  madugsum  21540  fiuncmp  22301  ptcld  22510  ptcldmpt  22511  ptclsg  22512  elmptrab  22724  prdsdsf  23265  prdsxmet  23267  fsumcn  23767  fsum2cn  23768  ovolfiniun  24398  ovoliunlem3  24401  ovoliun  24402  ovoliun2  24403  ovoliunnul  24404  finiunmbl  24441  volfiniun  24444  iundisj  24445  iundisj2  24446  iunmbl  24450  iunmbl2  24454  itgss3  24712  itgfsum  24724  itgabs  24732  limciun  24791  dvmptfsum  24872  dvfsumle  24918  dvfsumabs  24920  dvfsumlem1  24923  dvfsumlem2  24924  dvfsumlem3  24925  dvfsumlem4  24926  dvfsumrlim  24928  dvfsumrlim2  24929  dvfsum2  24931  itgsubstlem  24945  itgsubst  24946  rlimcnp2  25849  fsumdvdscom  26067  fsumdvdsmul  26077  fsumvma  26094  dchrisumlema  26369  dchrisumlem2  26371  dchrisumlem3  26372  ifeqeqx  30604  disjorsf  30638  disjabrex  30640  disjabrexf  30641  iundisjf  30647  iundisj2f  30648  disjunsn  30652  suppss2f  30693  2ndresdju  30705  fmptdF  30713  fmptcof2  30714  acunirnmpt2f  30718  aciunf1lem  30719  funcnv4mpt  30726  f1od2  30776  iundisjfi  30837  iundisj2fi  30838  fsumiunle  30863  gsummpt2co  31027  gsumpart  31034  gsumvsca1  31198  gsumvsca2  31199  rmfsupp2  31211  esumpfinvalf  31756  esum2dlem  31772  esumiun  31774  fiunelros  31854  measiun  31898  voliune  31909  volfiniune  31910  sbcaltop  34020  bj-sbeqALT  34822  csbdif  35233  rdgssun  35286  finxpreclem2  35298  phpreu  35498  finixpnum  35499  ptrest  35513  poimirlem23  35537  poimirlem24  35538  poimirlem25  35539  poimirlem26  35540  poimirlem27  35541  poimirlem28  35542  mbfposadd  35561  itgabsnc  35583  ftc1cnnclem  35585  ftc2nc  35596  fsumshftd  36703  riotasv2s  36709  cdleme31sn  38131  cdleme31sn1  38132  cdleme31se2  38134  cdleme32fva  38188  cdleme42b  38229  hlhilset  39685  mzpsubst  40273  rabdiophlem2  40327  elnn0rabdioph  40328  dvdsrabdioph  40335  fphpd  40341  monotuz  40466  oddcomabszz  40469  aomclem6  40587  flcidc  40702  csbcog  40934  fsumcnf  42237  sumsnd  42242  elabrexg  42262  fiiuncl  42286  eliin2f  42327  disjf1  42393  disjrnmpt2  42399  disjinfi  42404  fmptf  42455  iuneqfzuzlem  42546  supxrleubrnmptf  42666  fsummulc1f  42787  fsumnncl  42788  fsumf1of  42790  fsumiunss  42791  fsumreclf  42792  fsumlessf  42793  fsumsermpt  42795  fprodexp  42810  fprodabs2  42811  mccllem  42813  fprodcnlem  42815  fprodcn  42816  climsubmpt  42876  climeldmeqmpt  42884  climfveqmpt  42887  climfveqmpt3  42898  climeldmeqmpt3  42905  climinf2mpt  42930  climinfmpt  42931  limsupequzmptf  42947  fprodcncf  43116  dvmptmulf  43153  dvnmptdivc  43154  dvmptfprod  43161  iblsplitf  43186  fourierdlem86  43408  fourierdlem112  43434  sge0f1o  43595  sge0lempt  43623  sge0iunmptlemfi  43626  sge0iunmptlemre  43628  sge0iunmpt  43631  sge0ltfirpmpt2  43639  sge0isummpt2  43645  sge0xaddlem2  43647  sge0xadd  43648  meadjiun  43679  hoimbl2  43878  vonhoire  43885  vonn0ioo2  43903  vonn0icc2  43905  csbafv12g  44301  csbaovg  44344  csbafv212g  44383  fsummsndifre  44497  fsumsplitsndif  44498  fsummmodsndifre  44499  fsummmodsnunz  44500  opeliun2xp  45341  dmmpossx2  45345