Theorem csbeq1a 3897

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

Syntax hints:   → wi 4   = wceq 1537  ⦋csb 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1540  df-ex 1781  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-sbc 3773  df-csb 3884

This theorem is referenced by:  csbhypf  3911  csbiebt  3912  cbvrabcsfw  3924  cbvralcsf  3925  cbvreucsf  3927  cbvrabcsf  3928  rspc2vd  3932  sbcnestgfw  4370  sbcnestgf  4375  csbun  4390  csbin  4391  csbif  4522  disjors  5047  invdisjrabw  5051  invdisjrab  5052  disjxiun  5063  disjxun  5064  sbcbr123  5120  eusvnf  5293  reusv2lem4  5302  reusv2  5304  moop2  5392  iunopeqop  5411  pofun  5491  opeliunxp  5619  elrnmpt1  5830  resmptf  5907  csbima12  5947  fvmpt2f  6769  fvmpts  6771  fvmptdf  6774  fvmpt2i  6778  fvmptex  6782  fmptco  6891  fmptcof  6892  fmptcos  6893  elabrex  7002  fliftfuns  7067  riotaeqimp  7140  csbov123  7198  ovmpos  7298  ofmpteq  7428  csbopeq1a  7749  mpomptsx  7762  dmmpossx  7764  fmpox  7765  el2mpocsbcl  7780  offval22  7783  ovmptss  7788  fmpoco  7790  mpoxeldm  7877  mpocurryd  7935  mpocurryvald  7936  fvmpocurryd  7937  eqerlem  8323  qliftfuns  8384  mptelixpg  8499  boxcutc  8505  xpf1o  8679  iunfi  8812  wdom2d  9044  ixpiunwdom  9055  hsmexlem2  9849  ac6c4  9903  iundom2g  9962  seqof2  13429  rlimcld2  14935  sumeq2ii  15050  summolem3  15071  summolem2a  15072  zsum  15075  fsum  15077  sumss2  15083  fsumcvg2  15084  fsumzcl2  15095  fsumsplitf  15098  sumsnf  15099  sumsns  15105  fsummsnunz  15109  fsumsplitsnun  15110  fsum2dlem  15125  fsumcnv  15128  fsumcom2  15129  fsumshftm  15136  fsum0diag2  15138  fsum00  15153  fsumabs  15156  fsumrlim  15166  fsumo1  15167  o1fsum  15168  fsumiun  15176  infcvgaux1i  15212  prodeq2ii  15267  prodmolem3  15287  prodmolem2a  15288  zprod  15291  fprod  15295  fprodntriv  15296  prodss  15301  fprodser  15303  fprodcllemf  15312  prodsn  15316  prodsnf  15318  fprodm1s  15324  fprodp1s  15325  prodsns  15326  fprodabs  15328  fprodn0  15333  fprod2dlem  15334  fprodcnv  15337  fprodcom2  15338  fproddivf  15341  fprodsplitf  15342  fprodsplit1f  15344  fprodle  15350  fprodmodd  15351  fprodefsum  15448  sumeven  15738  sumodd  15739  pcmpt  16228  pcmptdvds  16230  natpropd  17246  fucpropd  17247  gsummpt1n0  19085  gsumcom2  19095  gsummptnn0fz  19106  dprd2d2  19166  psrass1lem  20157  mpfrcl  20298  coe1fzgsumdlem  20469  gsumply1eq  20473  evl1gsumdlem  20519  mdetralt2  21218  mdetunilem2  21222  madugsum  21252  fiuncmp  22012  ptcld  22221  ptcldmpt  22222  ptclsg  22223  elmptrab  22435  prdsdsf  22977  prdsxmet  22979  fsumcn  23478  fsum2cn  23479  ovolfiniun  24102  ovoliunlem3  24105  ovoliun  24106  ovoliun2  24107  ovoliunnul  24108  finiunmbl  24145  volfiniun  24148  iundisj  24149  iundisj2  24150  iunmbl  24154  iunmbl2  24158  itgss3  24415  itgfsum  24427  itgabs  24435  limciun  24492  dvmptfsum  24572  dvfsumle  24618  dvfsumabs  24620  dvfsumlem1  24623  dvfsumlem2  24624  dvfsumlem3  24625  dvfsumlem4  24626  dvfsumrlim  24628  dvfsumrlim2  24629  dvfsum2  24631  itgsubstlem  24645  itgsubst  24646  rlimcnp2  25544  fsumdvdscom  25762  fsumdvdsmul  25772  fsumvma  25789  dchrisumlema  26064  dchrisumlem2  26066  dchrisumlem3  26067  ifeqeqx  30297  disjorsf  30330  disjabrex  30332  disjabrexf  30333  iundisjf  30339  iundisj2f  30340  disjunsn  30344  suppss2f  30384  fmptdF  30401  fmptcof2  30402  acunirnmpt2f  30406  aciunf1lem  30407  funcnv4mpt  30414  f1od2  30457  iundisjfi  30519  iundisj2fi  30520  fsumiunle  30545  gsummpt2co  30686  gsumvsca1  30854  gsumvsca2  30855  rmfsupp2  30866  esumpfinvalf  31335  esum2dlem  31351  esumiun  31353  fiunelros  31433  measiun  31477  voliune  31488  volfiniune  31489  sbcaltop  33442  bj-sbeqALT  34220  csbdif  34609  rdgssun  34662  finxpreclem2  34674  phpreu  34891  finixpnum  34892  ptrest  34906  poimirlem23  34930  poimirlem24  34931  poimirlem25  34932  poimirlem26  34933  poimirlem27  34934  poimirlem28  34935  mbfposadd  34954  itgabsnc  34976  ftc1cnnclem  34980  ftc2nc  34991  fsumshftd  36103  riotasv2s  36109  cdleme31sn  37531  cdleme31sn1  37532  cdleme31se2  37534  cdleme32fva  37588  cdleme42b  37629  hlhilset  39085  mzpsubst  39365  rabdiophlem2  39419  elnn0rabdioph  39420  dvdsrabdioph  39427  fphpd  39433  monotuz  39558  oddcomabszz  39561  aomclem6  39679  flcidc  39794  csbcog  40014  fsumcnf  41298  sumsnd  41303  elabrexg  41323  fiiuncl  41347  eliin2f  41390  disjf1  41463  disjrnmpt2  41469  disjinfi  41474  fmptf  41529  iuneqfzuzlem  41622  supxrleubrnmptf  41747  fsumclf  41870  fsummulc1f  41871  fsumnncl  41872  fsumsplit1  41873  fsumf1of  41875  fsumiunss  41876  fsumreclf  41877  fsumlessf  41878  fsumsermpt  41880  fprodexp  41895  fprodabs2  41896  mccllem  41898  fprodcnlem  41900  fprodcn  41901  climsubmpt  41961  climeldmeqmpt  41969  climfveqmpt  41972  climfveqmpt3  41983  climeldmeqmpt3  41990  climinf2mpt  42015  climinfmpt  42016  limsupequzmptf  42032  fprodcncf  42204  dvmptmulf  42242  dvnmptdivc  42243  dvmptfprod  42250  iblsplitf  42275  fourierdlem86  42497  fourierdlem112  42523  sge0f1o  42684  sge0lempt  42712  sge0iunmptlemfi  42715  sge0iunmptlemre  42717  sge0iunmpt  42720  sge0ltfirpmpt2  42728  sge0isummpt2  42734  sge0xaddlem2  42736  sge0xadd  42737  meadjiun  42768  hoimbl2  42967  vonhoire  42974  vonn0ioo2  42992  vonn0icc2  42994  csbafv12g  43356  csbaovg  43399  csbafv212g  43438  fsummsndifre  43552  fsumsplitsndif  43553  fsummmodsndifre  43554  fsummmodsnunz  43555  opeliun2xp  44401  dmmpossx2  44405