Theorem csbeq1a 3864

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ⦋csb 3850

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-12 2215  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-sbc 3743  df-csb 3851

This theorem is used by:  csbhypf  3878  csbiebt  3879  cbvrabcsfw  3891  cbvralcsf  3892  cbvreucsf  3894  cbvrabcsf  3895  rspc2vd  3898  sbcnestgfw  4382  sbcnestgf  4387  csbun  4402  csbin  4403  csbdif  4484  csbif  4543  disjors  5090  invdisjrab  5094  disjxiun  5104  disjxun  5105  sbcbr123  5163  eusvnf  5361  reusv2lem4  5370  reusv2  5372  moop2  5483  iunopeqop  5502  iunopeqopOLD  5503  pofun  5585  opeliunxp  5726  opeliun2xp  5727  elrnmpt1  5948  resmptf  6039  csbima12  6079  csbcog  6299  fvmpt2f  6991  fvmpts  6994  fvmptdf  6997  fvmpt2i  7001  fvmptex  7005  fmptco  7126  fmptcof  7127  fmptcos  7128  elabrex  7242  elabrexg  7243  fliftfuns  7318  riotaeqimp  7399  csbov123  7460  ovmpos  7564  fvmpopr2d  7578  ofmpteq  7704  csbopeq1a  8050  mpomptsx  8064  dmmpossx  8066  fmpox  8067  el2mpocsbcl  8085  offval22  8088  ovmptss  8093  fmpoco  8095  mpoxeldm  8212  mpocurryd  8270  mpocurryvald  8271  fvmpocurryd  8272  eqerlem  8735  qliftfuns  8807  mptelixpg  8945  boxcutc  8951  xpf1o  9140  iunfi  9313  wdom2d  9555  ixpiunwdom  9565  hsmexlem2  10432  ac6c4  10486  iundom2g  10551  seqof2  14126  rlimcld2  15667  sumeq2ii  15782  summolem3  15802  summolem2a  15803  zsum  15806  fsum  15808  sumss2  15814  fsumcvg2  15815  fsumclf  15826  fsumzcl2  15827  fsumsplitf  15830  sumsnf  15831  fsumsplit1  15833  sumsns  15838  fsummsnunz  15842  fsumsplitsnun  15843  fsum2dlem  15858  fsumcnv  15861  fsumcom2  15862  fsumshftm  15869  fsum0diag2  15871  fsum00  15887  fsumabs  15890  fsumrlim  15900  fsumo1  15901  o1fsum  15902  fsumiun  15910  infcvgaux1i  15948  prodeq2ii  16002  prodmolem3  16024  prodmolem2a  16025  zprod  16028  fprod  16032  fprodntriv  16033  prodss  16038  fprodser  16040  fprodcllemf  16049  prodsn  16053  prodsnf  16055  fprodm1s  16061  fprodp1s  16062  prodsns  16063  fprodabs  16065  fprodn0  16070  fprod2dlem  16071  fprodcnv  16074  fprodcom2  16075  fproddivf  16078  fprodsplitf  16079  fprodsplit1f  16081  fprodle  16087  fprodmodd  16088  fprodefsum  16185  sumeven  16481  sumodd  16482  pcmpt  16988  pcmptdvds  16990  natpropd  18072  fucpropd  18073  gsummpt1n0  20093  gsumcom2  20103  gsummptnn0fz  20114  dprd2d2  20174  psrass1lem  22149  mpfrcl  22302  coe1fzgsumdlem  22529  gsumply1eq  22535  evl1gsumdlem  22582  mdetralt2  22832  mdetunilem2  22836  madugsum  22866  fiuncmp  23630  ptcld  23840  ptcldmpt  23841  ptclsg  23842  elmptrab  24054  prdsdsf  24594  prdsxmet  24596  fsumcn  25099  fsum2cn  25100  ovolfiniun  25730  ovoliunlem3  25733  ovoliun  25734  ovoliun2  25735  ovoliunnul  25736  finiunmbl  25773  volfiniun  25776  iundisj  25777  iundisj2  25778  iunmbl  25782  iunmbl2  25786  itgss3  26044  itgfsum  26056  itgabs  26064  limciun  26123  dvmptfsum  26204  dvfsumle  26250  dvfsumabs  26252  dvfsumlem1  26255  dvfsumlem2  26256  dvfsumlem3  26257  dvfsumlem4  26258  dvfsumrlim  26260  dvfsumrlim2  26261  dvfsum2  26263  itgsubstlem  26277  itgsubst  26278  rlimcnp2  27201  fsumdvdscom  27419  fsumdvdsmul  27429  fsumvma  27447  dchrisumlema  27722  dchrisumlem2  27724  dchrisumlem3  27725  ifeqeqx  33003  iunxpssiun1  33028  disjorsf  33040  disjabrex  33042  disjabrexf  33043  iundisjf  33049  iundisj2f  33050  disjunsn  33054  suppss2f  33098  2ndresdju  33109  fmptdf2  33116  fmptcof2  33117  acunirnmpt2f  33121  aciunf1lem  33122  funcnv4mpt  33128  f1od2  33177  iundisjfi  33254  iundisj2fi  33255  fsumiunle  33286  gsummpt2co  33475  gsummptp1  33484  gsumpart  33490  gsumvsca1  33653  gsumvsca2  33654  rmfsupp2  33664  esumpfinvalf  34573  esum2dlem  34589  esumiun  34591  fiunelros  34672  measiun  34716  voliune  34727  volfiniune  34728  sbcaltop  36548  weiunpo  37071  weiunso  37072  weiunfr  37073  weiunse  37074  csbttc  37115  bj-sbeqALT  37630  rdgssun  38119  finxpreclem2  38131  phpreu  38345  finixpnum  38346  ptrest  38355  poimirlem23  38379  poimirlem24  38380  poimirlem25  38381  poimirlem26  38382  poimirlem27  38383  poimirlem28  38384  mbfposadd  38403  itgabsnc  38425  ftc1cnnclem  38427  ftc2nc  38438  fsumshftd  39812  riotasv2s  39818  cdleme31sn  41240  cdleme31sn1  41241  cdleme31se2  41243  cdleme32fva  41297  cdleme42b  41338  hlhilset  42794  evl1gprodd  42970  idomnnzgmulnz  42986  deg1gprod  42993  fmpocos  43090  mzpsubst  43580  rabdiophlem2  43630  elnn0rabdioph  43631  dvdsrabdioph  43638  fphpd  43644  monotuz  43769  oddcomabszz  43772  aomclem6  43887  flcidc  43998  fsumcnf  45842  sumsnd  45847  fiiuncl  45886  eliin2f  45923  disjf1  46002  disjrnmpt2  46007  disjinfi  46011  fmptf  46055  fmptff  46085  iuneqfzuzlem  46151  supxrleubrnmptf  46266  fsummulc1f  46388  fsumnncl  46389  fsumf1of  46391  fsumiunss  46392  fsumreclf  46393  fsumlessf  46394  fsumsermpt  46396  fprodexp  46411  fprodabs2  46412  mccllem  46414  fprodcnlem  46416  fprodcn  46417  climsubmpt  46475  climeldmeqmpt  46483  climfveqmpt  46486  climfveqmpt3  46497  climeldmeqmpt3  46504  climinf2mpt  46529  climinfmpt  46530  limsupequzmptf  46546  fprodcncf  46715  dvmptmulf  46752  dvnmptdivc  46753  dvmptfprod  46760  iblsplitf  46785  fourierdlem86  47007  fourierdlem112  47033  sge0f1o  47197  sge0lempt  47225  sge0iunmptlemfi  47228  sge0iunmptlemre  47230  sge0iunmpt  47233  sge0ltfirpmpt2  47241  sge0isummpt2  47247  sge0xaddlem2  47249  sge0xadd  47250  meadjiun  47281  hoimbl2  47480  vonhoire  47487  vonn0ioo2  47505  vonn0icc2  47507  csbafv12g  48012  csbaovg  48055  csbafv212g  48094  fsummsndifre  48255  fsumsplitsndif  48256  fsummmodsndifre  48257  fsummmodsnunz  48258  dmmpossx2  49254