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  7077  fmptcof  7078  fmptcos  7079  elabrex  7191  elabrexg  7192  fliftfuns  7263  riotaeqimp  7344  csbov123  7405  ovmpos  7509  fvmpopr2d  7523  ofmpteq  7648  csbopeq1a  7997  mpomptsx  8011  dmmpossx  8013  fmpox  8014  el2mpocsbcl  8030  offval22  8033  ovmptss  8038  fmpoco  8040  mpoxeldm  8156  mpocurryd  8214  mpocurryvald  8215  fvmpocurryd  8216  eqerlem  8674  qliftfuns  8746  mptelixpg  8878  boxcutc  8884  xpf1o  9072  iunfi  9248  wdom2d  9490  ixpiunwdom  9500  hsmexlem2  10342  ac6c4  10396  iundom2g  10455  seqof2  13988  rlimcld2  15506  sumeq2ii  15621  summolem3  15642  summolem2a  15643  zsum  15646  fsum  15648  sumss2  15654  fsumcvg2  15655  fsumclf  15666  fsumzcl2  15667  fsumsplitf  15670  sumsnf  15671  fsumsplit1  15673  sumsns  15678  fsummsnunz  15682  fsumsplitsnun  15683  fsum2dlem  15698  fsumcnv  15701  fsumcom2  15702  fsumshftm  15709  fsum0diag2  15711  fsum00  15726  fsumabs  15729  fsumrlim  15739  fsumo1  15740  o1fsum  15741  fsumiun  15749  infcvgaux1i  15785  prodeq2ii  15839  prodmolem3  15861  prodmolem2a  15862  zprod  15865  fprod  15869  fprodntriv  15870  prodss  15875  fprodser  15877  fprodcllemf  15886  prodsn  15890  prodsnf  15892  fprodm1s  15898  fprodp1s  15899  prodsns  15900  fprodabs  15902  fprodn0  15907  fprod2dlem  15908  fprodcnv  15911  fprodcom2  15912  fproddivf  15915  fprodsplitf  15916  fprodsplit1f  15918  fprodle  15924  fprodmodd  15925  fprodefsum  16023  sumeven  16319  sumodd  16320  pcmpt  16825  pcmptdvds  16827  natpropd  17908  fucpropd  17909  gsummpt1n0  19899  gsumcom2  19909  gsummptnn0fz  19920  dprd2d2  19980  psrass1lem  21893  mpfrcl  22045  coe1fzgsumdlem  22252  gsumply1eq  22258  evl1gsumdlem  22305  mdetralt2  22558  mdetunilem2  22562  madugsum  22592  fiuncmp  23353  ptcld  23562  ptcldmpt  23563  ptclsg  23564  elmptrab  23776  prdsdsf  24316  prdsxmet  24318  fsumcn  24822  fsum2cn  24823  ovolfiniun  25463  ovoliunlem3  25466  ovoliun  25467  ovoliun2  25468  ovoliunnul  25469  finiunmbl  25506  volfiniun  25509  iundisj  25510  iundisj2  25511  iunmbl  25515  iunmbl2  25519  itgss3  25777  itgfsum  25789  itgabs  25797  limciun  25856  dvmptfsum  25940  dvfsumle  25987  dvfsumleOLD  25988  dvfsumabs  25990  dvfsumlem1  25993  dvfsumlem2  25994  dvfsumlem2OLD  25995  dvfsumlem3  25996  dvfsumlem4  25997  dvfsumrlim  25999  dvfsumrlim2  26000  dvfsum2  26002  itgsubstlem  26016  itgsubst  26017  rlimcnp2  26937  fsumdvdscom  27156  fsumdvdsmul  27166  fsumdvdsmulOLD  27168  fsumvma  27185  dchrisumlema  27460  dchrisumlem2  27462  dchrisumlem3  27463  ifeqeqx  32621  iunxpssiun1  32647  disjorsf  32659  disjabrex  32661  disjabrexf  32662  iundisjf  32668  iundisj2f  32669  disjunsn  32673  suppss2f  32720  2ndresdju  32731  fmptdF  32738  fmptcof2  32739  acunirnmpt2f  32743  aciunf1lem  32744  funcnv4mpt  32750  f1od2  32801  iundisjfi  32879  iundisj2fi  32880  fsumiunle  32913  gsummpt2co  33134  gsummptp1  33143  gsumpart  33149  gsumvsca1  33312  gsumvsca2  33313  rmfsupp2  33324  esumpfinvalf  34246  esum2dlem  34262  esumiun  34264  fiunelros  34344  measiun  34388  voliune  34399  volfiniune  34400  sbcaltop  36188  weiunpo  36672  weiunso  36673  weiunfr  36674  weiunse  36675  bj-sbeqALT  37114  rdgssun  37596  finxpreclem2  37608  phpreu  37818  finixpnum  37819  ptrest  37833  poimirlem23  37857  poimirlem24  37858  poimirlem25  37859  poimirlem26  37860  poimirlem27  37861  poimirlem28  37862  mbfposadd  37881  itgabsnc  37903  ftc1cnnclem  37905  ftc2nc  37916  fsumshftd  39291  riotasv2s  39297  cdleme31sn  40719  cdleme31sn1  40720  cdleme31se2  40722  cdleme32fva  40776  cdleme42b  40817  hlhilset  42273  evl1gprodd  42450  idomnnzgmulnz  42466  deg1gprod  42473  fmpocos  42569  mzpsubst  43068  rabdiophlem2  43122  elnn0rabdioph  43123  dvdsrabdioph  43130  fphpd  43136  monotuz  43261  oddcomabszz  43264  aomclem6  43379  flcidc  43490  fsumcnf  45344  sumsnd  45349  fiiuncl  45388  eliin2f  45426  disjf1  45505  disjrnmpt2  45510  disjinfi  45514  fmptf  45560  fmptff  45590  iuneqfzuzlem  45656  supxrleubrnmptf  45772  fsummulc1f  45894  fsumnncl  45895  fsumf1of  45897  fsumiunss  45898  fsumreclf  45899  fsumlessf  45900  fsumsermpt  45902  fprodexp  45917  fprodabs2  45918  mccllem  45920  fprodcnlem  45922  fprodcn  45923  climsubmpt  45981  climeldmeqmpt  45989  climfveqmpt  45992  climfveqmpt3  46003  climeldmeqmpt3  46010  climinf2mpt  46035  climinfmpt  46036  limsupequzmptf  46052  fprodcncf  46221  dvmptmulf  46258  dvnmptdivc  46259  dvmptfprod  46266  iblsplitf  46291  fourierdlem86  46513  fourierdlem112  46539  sge0f1o  46703  sge0lempt  46731  sge0iunmptlemfi  46734  sge0iunmptlemre  46736  sge0iunmpt  46739  sge0ltfirpmpt2  46747  sge0isummpt2  46753  sge0xaddlem2  46755  sge0xadd  46756  meadjiun  46787  hoimbl2  46986  vonhoire  46993  vonn0ioo2  47011  vonn0icc2  47013  csbafv12g  47460  csbaovg  47503  csbafv212g  47542  fsummsndifre  47695  fsumsplitsndif  47696  fsummmodsndifre  47697  fsummmodsnunz  47698  dmmpossx2  48660