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 2812	1 ⊢ (𝑥 = 𝐴 → 𝐵 = ⦋𝐴 / 𝑥⦌𝐵)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1564  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-sbc 3746  df-csb 3854

This theorem is referenced by:  csbhypf  3881  csbiebt  3882  cbvrabcsfw  3894  cbvralcsf  3895  cbvreucsf  3897  cbvrabcsf  3898  rspc2vd  3901  sbcnestgfw  4376  sbcnestgf  4381  csbun  4396  csbin  4397  csbdif  4480  csbif  4539  disjors  5084  invdisjrab  5088  disjxiun  5098  disjxun  5099  sbcbr123  5155  eusvnf  5350  reusv2lem4  5359  reusv2  5361  moop2  5472  iunopeqop  5491  iunopeqopOLD  5492  pofun  5574  opeliunxp  5715  opeliun2xp  5716  elrnmpt1  5937  resmptf  6028  csbima12  6068  csbcog  6284  fvmpt2f  6976  fvmpts  6979  fvmptdf  6982  fvmpt2i  6986  fvmptex  6990  fmptco  7111  fmptcof  7112  fmptcos  7113  elabrex  7226  elabrexg  7227  fliftfuns  7298  riotaeqimp  7379  csbov123  7440  ovmpos  7544  fvmpopr2d  7558  ofmpteq  7683  csbopeq1a  8031  mpomptsx  8045  dmmpossx  8047  fmpox  8048  el2mpocsbcl  8064  offval22  8067  ovmptss  8072  fmpoco  8074  mpoxeldm  8191  mpocurryd  8249  mpocurryvald  8250  fvmpocurryd  8251  eqerlem  8714  qliftfuns  8786  mptelixpg  8917  boxcutc  8923  xpf1o  9111  iunfi  9284  wdom2d  9526  ixpiunwdom  9536  hsmexlem2  10395  ac6c4  10449  iundom2g  10508  seqof2  14083  rlimcld2  15615  sumeq2ii  15730  summolem3  15751  summolem2a  15752  zsum  15755  fsum  15757  sumss2  15763  fsumcvg2  15764  fsumclf  15775  fsumzcl2  15776  fsumsplitf  15779  sumsnf  15780  fsumsplit1  15782  sumsns  15787  fsummsnunz  15791  fsumsplitsnun  15792  fsum2dlem  15807  fsumcnv  15810  fsumcom2  15811  fsumshftm  15818  fsum0diag2  15820  fsum00  15836  fsumabs  15839  fsumrlim  15849  fsumo1  15850  o1fsum  15851  fsumiun  15859  infcvgaux1i  15897  prodeq2ii  15951  prodmolem3  15973  prodmolem2a  15974  zprod  15977  fprod  15981  fprodntriv  15982  prodss  15987  fprodser  15989  fprodcllemf  15998  prodsn  16002  prodsnf  16004  fprodm1s  16010  fprodp1s  16011  prodsns  16012  fprodabs  16014  fprodn0  16019  fprod2dlem  16020  fprodcnv  16023  fprodcom2  16024  fproddivf  16027  fprodsplitf  16028  fprodsplit1f  16030  fprodle  16036  fprodmodd  16037  fprodefsum  16135  sumeven  16431  sumodd  16432  pcmpt  16938  pcmptdvds  16940  natpropd  18022  fucpropd  18023  gsummpt1n0  20015  gsumcom2  20025  gsummptnn0fz  20036  dprd2d2  20096  psrass1lem  21992  mpfrcl  22145  coe1fzgsumdlem  22373  gsumply1eq  22379  evl1gsumdlem  22426  mdetralt2  22676  mdetunilem2  22680  madugsum  22710  fiuncmp  23471  ptcld  23680  ptcldmpt  23681  ptclsg  23682  elmptrab  23894  prdsdsf  24434  prdsxmet  24436  fsumcn  24939  fsum2cn  24940  ovolfiniun  25570  ovoliunlem3  25573  ovoliun  25574  ovoliun2  25575  ovoliunnul  25576  finiunmbl  25613  volfiniun  25616  iundisj  25617  iundisj2  25618  iunmbl  25622  iunmbl2  25626  itgss3  25884  itgfsum  25896  itgabs  25904  limciun  25963  dvmptfsum  26044  dvfsumle  26090  dvfsumabs  26092  dvfsumlem1  26095  dvfsumlem2  26096  dvfsumlem3  26097  dvfsumlem4  26098  dvfsumrlim  26100  dvfsumrlim2  26101  dvfsum2  26103  itgsubstlem  26117  itgsubst  26118  rlimcnp2  27038  fsumdvdscom  27256  fsumdvdsmul  27266  fsumvma  27284  dchrisumlema  27559  dchrisumlem2  27561  dchrisumlem3  27562  ifeqeqx  32747  iunxpssiun1  32774  disjorsf  32786  disjabrex  32788  disjabrexf  32789  iundisjf  32795  iundisj2f  32796  disjunsn  32800  suppss2f  32846  2ndresdju  32857  fmptdF  32864  fmptcof2  32865  acunirnmpt2f  32869  aciunf1lem  32870  funcnv4mpt  32876  f1od2  32927  iundisjfi  33004  iundisj2fi  33005  fsumiunle  33037  gsummpt2co  33234  gsummptp1  33243  gsumpart  33249  gsumvsca1  33412  gsumvsca2  33413  rmfsupp2  33424  esumpfinvalf  34375  esum2dlem  34391  esumiun  34393  fiunelros  34473  measiun  34517  voliune  34528  volfiniune  34529  sbcaltop  36336  weiunpo  36830  weiunso  36831  weiunfr  36832  weiunse  36833  csbttc  36874  bj-sbeqALT  37390  rdgssun  37877  finxpreclem2  37889  phpreu  38108  finixpnum  38109  ptrest  38123  poimirlem23  38147  poimirlem24  38148  poimirlem25  38149  poimirlem26  38150  poimirlem27  38151  poimirlem28  38152  mbfposadd  38171  itgabsnc  38193  ftc1cnnclem  38195  ftc2nc  38206  fsumshftd  39581  riotasv2s  39587  cdleme31sn  41009  cdleme31sn1  41010  cdleme31se2  41012  cdleme32fva  41066  cdleme42b  41107  hlhilset  42563  evl1gprodd  42739  idomnnzgmulnz  42755  deg1gprod  42762  fmpocos  42857  mzpsubst  43334  rabdiophlem2  43384  elnn0rabdioph  43385  dvdsrabdioph  43392  fphpd  43398  monotuz  43523  oddcomabszz  43526  aomclem6  43641  flcidc  43752  fsumcnf  45592  sumsnd  45597  fiiuncl  45636  eliin2f  45673  disjf1  45752  disjrnmpt2  45757  disjinfi  45761  fmptf  45805  fmptff  45835  iuneqfzuzlem  45901  supxrleubrnmptf  46016  fsummulc1f  46138  fsumnncl  46139  fsumf1of  46141  fsumiunss  46142  fsumreclf  46143  fsumlessf  46144  fsumsermpt  46146  fprodexp  46161  fprodabs2  46162  mccllem  46164  fprodcnlem  46166  fprodcn  46167  climsubmpt  46225  climeldmeqmpt  46233  climfveqmpt  46236  climfveqmpt3  46247  climeldmeqmpt3  46254  climinf2mpt  46279  climinfmpt  46280  limsupequzmptf  46296  fprodcncf  46465  dvmptmulf  46502  dvnmptdivc  46503  dvmptfprod  46510  iblsplitf  46535  fourierdlem86  46757  fourierdlem112  46783  sge0f1o  46947  sge0lempt  46975  sge0iunmptlemfi  46978  sge0iunmptlemre  46980  sge0iunmpt  46983  sge0ltfirpmpt2  46991  sge0isummpt2  46997  sge0xaddlem2  46999  sge0xadd  47000  meadjiun  47031  hoimbl2  47230  vonhoire  47237  vonn0ioo2  47255  vonn0icc2  47257  csbafv12g  47722  csbaovg  47765  csbafv212g  47804  fsummsndifre  47965  fsumsplitsndif  47966  fsummmodsndifre  47967  fsummmodsnunz  47968  dmmpossx2  48950