Theorem csbeq1a 3795

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 3794	. 2 ⊢ ⦋𝑥 / 𝑥⦌𝐵 = 𝐵
2		csbeq1 3789	. 2 ⊢ (𝑥 = 𝐴 → ⦋𝑥 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
3	1, 2	syl5eqr 2828	1 ⊢ (𝑥 = 𝐴 → 𝐵 = ⦋𝐴 / 𝑥⦌𝐵)

Syntax hints:   → wi 4   = wceq 1507  ⦋csb 3786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-12 2106  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-tru 1510  df-ex 1743  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-sbc 3682  df-csb 3787

This theorem is referenced by:  csbhypf  3807  csbiebt  3808  cbvralcsf  3820  cbvreucsf  3822  cbvrabcsf  3823  sbcnestgf  4259  csbun  4274  csbin  4275  csbif  4405  disjors  4912  invdisjrab  4916  disjxiun  4926  disjxun  4927  sbcbr123  4983  eusvnf  5146  reusv2lem4  5155  reusv2  5157  moop2  5248  iunopeqop  5267  pofun  5343  opeliunxp  5469  elrnmpt1  5673  resmptf  5752  csbima12  5787  fvmpt2f  6596  fvmpts  6598  fvmpt2i  6604  fvmptex  6608  fmptco  6714  fmptcof  6715  fmptcos  6716  elabrex  6827  fliftfuns  6890  riotaeqimp  6960  csbov123  7017  ovmpos  7114  ofmpteq  7246  csbopeq1a  7557  mpomptsx  7570  dmmpossx  7572  fmpox  7573  el2mpocsbcl  7588  offval22  7591  ovmptss  7596  fmpoco  7598  mpoxeldm  7680  mpocurryd  7738  mpocurryvald  7739  fvmpocurryd  7740  eqerlem  8123  qliftfuns  8184  mptelixpg  8296  boxcutc  8302  xpf1o  8475  iunfi  8607  wdom2d  8839  ixpiunwdom  8850  hsmexlem2  9647  ac6c4  9701  iundom2g  9760  seqof2  13243  rlimcld2  14796  sumeq2ii  14910  summolem3  14931  summolem2a  14932  zsum  14935  fsum  14937  sumss2  14943  fsumcvg2  14944  fsumzcl2  14955  fsumsplitf  14958  sumsnf  14959  sumsns  14965  fsummsnunz  14969  fsumsplitsnun  14970  fsum2dlem  14985  fsumcnv  14988  fsumcom2  14989  fsumshftm  14996  fsum0diag2  14998  fsum00  15013  fsumabs  15016  fsumrlim  15026  fsumo1  15027  o1fsum  15028  fsumiun  15036  infcvgaux1i  15072  prodeq2ii  15127  prodmolem3  15147  prodmolem2a  15148  zprod  15151  fprod  15155  fprodntriv  15156  prodss  15161  fprodser  15163  fprodcllemf  15172  prodsn  15176  prodsnf  15178  fprodm1s  15184  fprodp1s  15185  prodsns  15186  fprodabs  15188  fprodn0  15193  fprod2dlem  15194  fprodcnv  15197  fprodcom2  15198  fproddivf  15201  fprodsplitf  15202  fprodsplit1f  15204  fprodle  15210  fprodmodd  15211  fprodefsum  15308  sumeven  15598  sumodd  15599  pcmpt  16084  pcmptdvds  16086  natpropd  17104  fucpropd  17105  gsummpt1n0  18838  gsumcom2  18848  gsummptnn0fz  18856  dprd2d2  18916  psrass1lem  19871  mpfrcl  20011  coe1fzgsumdlem  20172  gsumply1eq  20176  evl1gsumdlem  20221  mdetralt2  20922  mdetunilem2  20926  madugsum  20956  fiuncmp  21716  ptcld  21925  ptcldmpt  21926  ptclsg  21927  elmptrab  22139  prdsdsf  22680  prdsxmet  22682  fsumcn  23181  fsum2cn  23182  ovolfiniun  23805  ovoliunlem3  23808  ovoliun  23809  ovoliun2  23810  ovoliunnul  23811  finiunmbl  23848  volfiniun  23851  iundisj  23852  iundisj2  23853  iunmbl  23857  iunmbl2  23861  itgss3  24118  itgfsum  24130  itgabs  24138  limciun  24195  dvmptfsum  24275  dvfsumle  24321  dvfsumabs  24323  dvfsumlem1  24326  dvfsumlem2  24327  dvfsumlem3  24328  dvfsumlem4  24329  dvfsumrlim  24331  dvfsumrlim2  24332  dvfsum2  24334  itgsubstlem  24348  itgsubst  24349  rlimcnp2  25246  fsumdvdscom  25464  fsumdvdsmul  25474  fsumvma  25491  dchrisumlema  25766  dchrisumlem2  25768  dchrisumlem3  25769  rspc2vd  27799  ifeqeqx  30065  disjorsf  30096  disjabrex  30098  disjabrexf  30099  iundisjf  30105  iundisj2f  30106  disjunsn  30110  suppss2f  30146  fmptdF  30163  fmptcof2  30164  acunirnmpt2f  30168  aciunf1lem  30169  funcnv4mpt  30176  f1od2  30216  iundisjfi  30275  iundisj2fi  30276  fsumiunle  30298  gsummpt2co  30529  gsumvsca1  30531  gsumvsca2  30532  rmfsupp2  30551  esumpfinvalf  30985  esum2dlem  31001  esumiun  31003  fiunelros  31084  measiun  31128  voliune  31139  volfiniune  31140  sbcaltop  32969  bj-sbeqALT  33715  csbdif  34054  rdgssun  34107  finxpreclem2  34118  phpreu  34323  finixpnum  34324  ptrest  34338  poimirlem23  34362  poimirlem24  34363  poimirlem25  34364  poimirlem26  34365  poimirlem27  34366  poimirlem28  34367  mbfposadd  34386  itgabsnc  34408  ftc1cnnclem  34412  ftc2nc  34423  fsumshftd  35539  riotasv2s  35545  cdleme31sn  36967  cdleme31sn1  36968  cdleme31se2  36970  cdleme32fva  37024  cdleme42b  37065  hlhilset  38521  mzpsubst  38746  rabdiophlem2  38801  elnn0rabdioph  38802  dvdsrabdioph  38809  fphpd  38815  monotuz  38940  oddcomabszz  38943  aomclem6  39061  flcidc  39176  csbcog  39363  fsumcnf  40703  sumsnd  40708  elabrexg  40728  fiiuncl  40752  eliin2f  40799  disjf1  40873  disjrnmpt2  40879  disjinfi  40884  fmptf  40942  iuneqfzuzlem  41037  supxrleubrnmptf  41164  fsumclf  41287  fsummulc1f  41288  fsumnncl  41289  fsumsplit1  41290  fsumf1of  41292  fsumiunss  41293  fsumreclf  41294  fsumlessf  41295  fsumsermpt  41297  fprodexp  41312  fprodabs2  41313  mccllem  41315  fprodcnlem  41317  fprodcn  41318  climsubmpt  41378  climeldmeqmpt  41386  climfveqmpt  41389  climfveqmpt3  41400  climeldmeqmpt3  41407  climinf2mpt  41432  climinfmpt  41433  limsupequzmptf  41449  fprodcncf  41620  dvmptmulf  41658  dvnmptdivc  41659  dvmptfprod  41666  iblsplitf  41691  fourierdlem86  41914  fourierdlem112  41940  sge0f1o  42101  sge0lempt  42129  sge0iunmptlemfi  42132  sge0iunmptlemre  42134  sge0iunmpt  42137  sge0ltfirpmpt2  42145  sge0isummpt2  42151  sge0xaddlem2  42153  sge0xadd  42154  meadjiun  42185  hoimbl2  42384  vonhoire  42391  vonn0ioo2  42409  vonn0icc2  42411  csbafv12g  42748  csbaovg  42791  csbafv212g  42830  fsummsndifre  42944  fsumsplitsndif  42945  fsummmodsndifre  42946  fsummmodsnunz  42947  opeliun2xp  43751  dmmpossx2  43755