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

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

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 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-sbc 3742  df-csb 3851

This theorem is referenced by:  csbhypf  3878  csbiebt  3879  cbvrabcsfw  3891  cbvralcsf  3892  cbvreucsf  3894  cbvrabcsf  3895  rspc2vd  3898  sbcnestgfw  4374  sbcnestgf  4379  csbun  4394  csbin  4395  csbdif  4479  csbif  4538  disjors  5082  invdisjrab  5086  disjxiun  5096  disjxun  5097  sbcbr123  5153  eusvnf  5338  reusv2lem4  5347  reusv2  5349  moop2  5451  iunopeqop  5470  pofun  5551  opeliunxp  5692  opeliun2xp  5693  elrnmpt1  5910  resmptf  5999  csbima12  6039  csbcog  6256  fvmpt2f  6943  fvmpts  6946  fvmptdf  6949  fvmpt2i  6953  fvmptex  6957  fmptco  7076  fmptcof  7077  fmptcos  7078  elabrex  7190  elabrexg  7191  fliftfuns  7262  riotaeqimp  7343  csbov123  7404  ovmpos  7508  fvmpopr2d  7522  ofmpteq  7647  csbopeq1a  7996  mpomptsx  8010  dmmpossx  8012  fmpox  8013  el2mpocsbcl  8029  offval22  8032  ovmptss  8037  fmpoco  8039  mpoxeldm  8155  mpocurryd  8213  mpocurryvald  8214  fvmpocurryd  8215  eqerlem  8673  qliftfuns  8745  mptelixpg  8877  boxcutc  8883  xpf1o  9071  iunfi  9247  wdom2d  9489  ixpiunwdom  9499  hsmexlem2  10341  ac6c4  10395  iundom2g  10454  seqof2  13987  rlimcld2  15505  sumeq2ii  15620  summolem3  15641  summolem2a  15642  zsum  15645  fsum  15647  sumss2  15653  fsumcvg2  15654  fsumclf  15665  fsumzcl2  15666  fsumsplitf  15669  sumsnf  15670  fsumsplit1  15672  sumsns  15677  fsummsnunz  15681  fsumsplitsnun  15682  fsum2dlem  15697  fsumcnv  15700  fsumcom2  15701  fsumshftm  15708  fsum0diag2  15710  fsum00  15725  fsumabs  15728  fsumrlim  15738  fsumo1  15739  o1fsum  15740  fsumiun  15748  infcvgaux1i  15784  prodeq2ii  15838  prodmolem3  15860  prodmolem2a  15861  zprod  15864  fprod  15868  fprodntriv  15869  prodss  15874  fprodser  15876  fprodcllemf  15885  prodsn  15889  prodsnf  15891  fprodm1s  15897  fprodp1s  15898  prodsns  15899  fprodabs  15901  fprodn0  15906  fprod2dlem  15907  fprodcnv  15910  fprodcom2  15911  fproddivf  15914  fprodsplitf  15915  fprodsplit1f  15917  fprodle  15923  fprodmodd  15924  fprodefsum  16022  sumeven  16318  sumodd  16319  pcmpt  16824  pcmptdvds  16826  natpropd  17907  fucpropd  17908  gsummpt1n0  19898  gsumcom2  19908  gsummptnn0fz  19919  dprd2d2  19979  psrass1lem  21892  mpfrcl  22044  coe1fzgsumdlem  22251  gsumply1eq  22257  evl1gsumdlem  22304  mdetralt2  22557  mdetunilem2  22561  madugsum  22591  fiuncmp  23352  ptcld  23561  ptcldmpt  23562  ptclsg  23563  elmptrab  23775  prdsdsf  24315  prdsxmet  24317  fsumcn  24821  fsum2cn  24822  ovolfiniun  25462  ovoliunlem3  25465  ovoliun  25466  ovoliun2  25467  ovoliunnul  25468  finiunmbl  25505  volfiniun  25508  iundisj  25509  iundisj2  25510  iunmbl  25514  iunmbl2  25518  itgss3  25776  itgfsum  25788  itgabs  25796  limciun  25855  dvmptfsum  25939  dvfsumle  25986  dvfsumleOLD  25987  dvfsumabs  25989  dvfsumlem1  25992  dvfsumlem2  25993  dvfsumlem2OLD  25994  dvfsumlem3  25995  dvfsumlem4  25996  dvfsumrlim  25998  dvfsumrlim2  25999  dvfsum2  26001  itgsubstlem  26015  itgsubst  26016  rlimcnp2  26936  fsumdvdscom  27155  fsumdvdsmul  27165  fsumdvdsmulOLD  27167  fsumvma  27184  dchrisumlema  27459  dchrisumlem2  27461  dchrisumlem3  27462  ifeqeqx  32599  iunxpssiun1  32625  disjorsf  32637  disjabrex  32639  disjabrexf  32640  iundisjf  32646  iundisj2f  32647  disjunsn  32651  suppss2f  32698  2ndresdju  32709  fmptdF  32716  fmptcof2  32717  acunirnmpt2f  32721  aciunf1lem  32722  funcnv4mpt  32728  f1od2  32779  iundisjfi  32857  iundisj2fi  32858  fsumiunle  32891  gsummpt2co  33112  gsummptp1  33121  gsumpart  33127  gsumvsca1  33289  gsumvsca2  33290  rmfsupp2  33301  esumpfinvalf  34214  esum2dlem  34230  esumiun  34232  fiunelros  34312  measiun  34356  voliune  34367  volfiniune  34368  sbcaltop  36156  weiunpo  36640  weiunso  36641  weiunfr  36642  weiunse  36643  bj-sbeqALT  37076  rdgssun  37554  finxpreclem2  37566  phpreu  37776  finixpnum  37777  ptrest  37791  poimirlem23  37815  poimirlem24  37816  poimirlem25  37817  poimirlem26  37818  poimirlem27  37819  poimirlem28  37820  mbfposadd  37839  itgabsnc  37861  ftc1cnnclem  37863  ftc2nc  37874  fsumshftd  39249  riotasv2s  39255  cdleme31sn  40677  cdleme31sn1  40678  cdleme31se2  40680  cdleme32fva  40734  cdleme42b  40775  hlhilset  42231  evl1gprodd  42408  idomnnzgmulnz  42424  deg1gprod  42431  fmpocos  42527  mzpsubst  43026  rabdiophlem2  43080  elnn0rabdioph  43081  dvdsrabdioph  43088  fphpd  43094  monotuz  43219  oddcomabszz  43222  aomclem6  43337  flcidc  43448  fsumcnf  45302  sumsnd  45307  fiiuncl  45346  eliin2f  45384  disjf1  45463  disjrnmpt2  45468  disjinfi  45472  fmptf  45519  fmptff  45549  iuneqfzuzlem  45615  supxrleubrnmptf  45731  fsummulc1f  45853  fsumnncl  45854  fsumf1of  45856  fsumiunss  45857  fsumreclf  45858  fsumlessf  45859  fsumsermpt  45861  fprodexp  45876  fprodabs2  45877  mccllem  45879  fprodcnlem  45881  fprodcn  45882  climsubmpt  45940  climeldmeqmpt  45948  climfveqmpt  45951  climfveqmpt3  45962  climeldmeqmpt3  45969  climinf2mpt  45994  climinfmpt  45995  limsupequzmptf  46011  fprodcncf  46180  dvmptmulf  46217  dvnmptdivc  46218  dvmptfprod  46225  iblsplitf  46250  fourierdlem86  46472  fourierdlem112  46498  sge0f1o  46662  sge0lempt  46690  sge0iunmptlemfi  46693  sge0iunmptlemre  46695  sge0iunmpt  46698  sge0ltfirpmpt2  46706  sge0isummpt2  46712  sge0xaddlem2  46714  sge0xadd  46715  meadjiun  46746  hoimbl2  46945  vonhoire  46952  vonn0ioo2  46970  vonn0icc2  46972  csbafv12g  47419  csbaovg  47462  csbafv212g  47501  fsummsndifre  47654  fsumsplitsndif  47655  fsummmodsndifre  47656  fsummmodsnunz  47657  dmmpossx2  48619