Theorem csbeq1a 3878

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

Syntax hints:   → wi 4   = wceq 1540  ⦋csb 3864

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-12 2178  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-sbc 3756  df-csb 3865

This theorem is referenced by:  csbhypf  3892  csbiebt  3893  cbvrabcsfw  3905  cbvralcsf  3906  cbvreucsf  3908  cbvrabcsf  3909  rspc2vd  3912  sbcnestgfw  4386  sbcnestgf  4391  csbun  4406  csbin  4407  csbdif  4489  csbif  4548  disjors  5092  invdisjrab  5096  disjxiun  5106  disjxun  5107  sbcbr123  5163  eusvnf  5349  reusv2lem4  5358  reusv2  5360  moop2  5464  iunopeqop  5483  pofun  5566  opeliunxp  5707  opeliun2xp  5708  elrnmpt1  5926  resmptf  6012  csbima12  6052  csbcog  6272  fvmpt2f  6971  fvmpts  6973  fvmptdf  6976  fvmpt2i  6980  fvmptex  6984  fmptco  7103  fmptcof  7104  fmptcos  7105  elabrex  7218  elabrexg  7219  fliftfuns  7291  riotaeqimp  7372  csbov123  7433  ovmpos  7539  fvmpopr2d  7553  ofmpteq  7678  csbopeq1a  8031  mpomptsx  8045  dmmpossx  8047  fmpox  8048  el2mpocsbcl  8066  offval22  8069  ovmptss  8074  fmpoco  8076  mpoxeldm  8192  mpocurryd  8250  mpocurryvald  8251  fvmpocurryd  8252  eqerlem  8708  qliftfuns  8779  mptelixpg  8910  boxcutc  8916  xpf1o  9108  iunfi  9300  wdom2d  9539  ixpiunwdom  9549  hsmexlem2  10386  ac6c4  10440  iundom2g  10499  seqof2  14031  rlimcld2  15550  sumeq2ii  15665  summolem3  15686  summolem2a  15687  zsum  15690  fsum  15692  sumss2  15698  fsumcvg2  15699  fsumclf  15710  fsumzcl2  15711  fsumsplitf  15714  sumsnf  15715  fsumsplit1  15717  sumsns  15722  fsummsnunz  15726  fsumsplitsnun  15727  fsum2dlem  15742  fsumcnv  15745  fsumcom2  15746  fsumshftm  15753  fsum0diag2  15755  fsum00  15770  fsumabs  15773  fsumrlim  15783  fsumo1  15784  o1fsum  15785  fsumiun  15793  infcvgaux1i  15829  prodeq2ii  15883  prodmolem3  15905  prodmolem2a  15906  zprod  15909  fprod  15913  fprodntriv  15914  prodss  15919  fprodser  15921  fprodcllemf  15930  prodsn  15934  prodsnf  15936  fprodm1s  15942  fprodp1s  15943  prodsns  15944  fprodabs  15946  fprodn0  15951  fprod2dlem  15952  fprodcnv  15955  fprodcom2  15956  fproddivf  15959  fprodsplitf  15960  fprodsplit1f  15962  fprodle  15968  fprodmodd  15969  fprodefsum  16067  sumeven  16363  sumodd  16364  pcmpt  16869  pcmptdvds  16871  natpropd  17947  fucpropd  17948  gsummpt1n0  19901  gsumcom2  19911  gsummptnn0fz  19922  dprd2d2  19982  psrass1lem  21847  mpfrcl  21998  coe1fzgsumdlem  22196  gsumply1eq  22202  evl1gsumdlem  22249  mdetralt2  22502  mdetunilem2  22506  madugsum  22536  fiuncmp  23297  ptcld  23506  ptcldmpt  23507  ptclsg  23508  elmptrab  23720  prdsdsf  24261  prdsxmet  24263  fsumcn  24767  fsum2cn  24768  ovolfiniun  25408  ovoliunlem3  25411  ovoliun  25412  ovoliun2  25413  ovoliunnul  25414  finiunmbl  25451  volfiniun  25454  iundisj  25455  iundisj2  25456  iunmbl  25460  iunmbl2  25464  itgss3  25722  itgfsum  25734  itgabs  25742  limciun  25801  dvmptfsum  25885  dvfsumle  25932  dvfsumleOLD  25933  dvfsumabs  25935  dvfsumlem1  25938  dvfsumlem2  25939  dvfsumlem2OLD  25940  dvfsumlem3  25941  dvfsumlem4  25942  dvfsumrlim  25944  dvfsumrlim2  25945  dvfsum2  25947  itgsubstlem  25961  itgsubst  25962  rlimcnp2  26882  fsumdvdscom  27101  fsumdvdsmul  27111  fsumdvdsmulOLD  27113  fsumvma  27130  dchrisumlema  27405  dchrisumlem2  27407  dchrisumlem3  27408  ifeqeqx  32477  iunxpssiun1  32503  disjorsf  32515  disjabrex  32517  disjabrexf  32518  iundisjf  32524  iundisj2f  32525  disjunsn  32529  suppss2f  32568  2ndresdju  32579  fmptdF  32586  fmptcof2  32587  acunirnmpt2f  32591  aciunf1lem  32592  funcnv4mpt  32599  f1od2  32650  iundisjfi  32725  iundisj2fi  32726  fsumiunle  32760  gsummpt2co  32994  gsumpart  33003  gsumvsca1  33185  gsumvsca2  33186  rmfsupp2  33195  esumpfinvalf  34072  esum2dlem  34088  esumiun  34090  fiunelros  34170  measiun  34214  voliune  34225  volfiniune  34226  sbcaltop  35964  weiunpo  36448  weiunso  36449  weiunfr  36450  weiunse  36451  bj-sbeqALT  36883  rdgssun  37361  finxpreclem2  37373  phpreu  37593  finixpnum  37594  ptrest  37608  poimirlem23  37632  poimirlem24  37633  poimirlem25  37634  poimirlem26  37635  poimirlem27  37636  poimirlem28  37637  mbfposadd  37656  itgabsnc  37678  ftc1cnnclem  37680  ftc2nc  37691  fsumshftd  38940  riotasv2s  38946  cdleme31sn  40369  cdleme31sn1  40370  cdleme31se2  40372  cdleme32fva  40426  cdleme42b  40467  hlhilset  41923  evl1gprodd  42100  idomnnzgmulnz  42116  deg1gprod  42123  fmpocos  42217  mzpsubst  42729  rabdiophlem2  42783  elnn0rabdioph  42784  dvdsrabdioph  42791  fphpd  42797  monotuz  42923  oddcomabszz  42926  aomclem6  43041  flcidc  43152  fsumcnf  45008  sumsnd  45013  fiiuncl  45052  eliin2f  45091  disjf1  45170  disjrnmpt2  45175  disjinfi  45179  fmptf  45226  fmptff  45256  iuneqfzuzlem  45323  supxrleubrnmptf  45440  fsummulc1f  45562  fsumnncl  45563  fsumf1of  45565  fsumiunss  45566  fsumreclf  45567  fsumlessf  45568  fsumsermpt  45570  fprodexp  45585  fprodabs2  45586  mccllem  45588  fprodcnlem  45590  fprodcn  45591  climsubmpt  45651  climeldmeqmpt  45659  climfveqmpt  45662  climfveqmpt3  45673  climeldmeqmpt3  45680  climinf2mpt  45705  climinfmpt  45706  limsupequzmptf  45722  fprodcncf  45891  dvmptmulf  45928  dvnmptdivc  45929  dvmptfprod  45936  iblsplitf  45961  fourierdlem86  46183  fourierdlem112  46209  sge0f1o  46373  sge0lempt  46401  sge0iunmptlemfi  46404  sge0iunmptlemre  46406  sge0iunmpt  46409  sge0ltfirpmpt2  46417  sge0isummpt2  46423  sge0xaddlem2  46425  sge0xadd  46426  meadjiun  46457  hoimbl2  46656  vonhoire  46663  vonn0ioo2  46681  vonn0icc2  46683  csbafv12g  47128  csbaovg  47171  csbafv212g  47210  fsummsndifre  47363  fsumsplitsndif  47364  fsummmodsndifre  47365  fsummmodsnunz  47366  dmmpossx2  48315