Theorem csbeq1a 3888

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

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

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 2007  ax-8 2110  ax-9 2118  ax-12 2177  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-sbc 3766  df-csb 3875

This theorem is referenced by:  csbhypf  3902  csbiebt  3903  cbvrabcsfw  3915  cbvralcsf  3916  cbvreucsf  3918  cbvrabcsf  3919  rspc2vd  3922  sbcnestgfw  4396  sbcnestgf  4401  csbun  4416  csbin  4417  csbdif  4499  csbif  4558  disjors  5102  invdisjrab  5106  disjxiun  5116  disjxun  5117  sbcbr123  5173  eusvnf  5362  reusv2lem4  5371  reusv2  5373  moop2  5477  iunopeqop  5496  pofun  5579  opeliunxp  5721  opeliun2xp  5722  elrnmpt1  5940  resmptf  6026  csbima12  6066  csbcog  6286  fvmpt2f  6986  fvmpts  6988  fvmptdf  6991  fvmpt2i  6995  fvmptex  6999  fmptco  7118  fmptcof  7119  fmptcos  7120  elabrex  7233  elabrexg  7234  fliftfuns  7306  riotaeqimp  7386  csbov123  7447  ovmpos  7553  fvmpopr2d  7567  ofmpteq  7692  csbopeq1a  8047  mpomptsx  8061  dmmpossx  8063  fmpox  8064  el2mpocsbcl  8082  offval22  8085  ovmptss  8090  fmpoco  8092  mpoxeldm  8208  mpocurryd  8266  mpocurryvald  8267  fvmpocurryd  8268  eqerlem  8752  qliftfuns  8816  mptelixpg  8947  boxcutc  8953  xpf1o  9151  iunfi  9353  wdom2d  9592  ixpiunwdom  9602  hsmexlem2  10439  ac6c4  10493  iundom2g  10552  seqof2  14076  rlimcld2  15592  sumeq2ii  15707  summolem3  15728  summolem2a  15729  zsum  15732  fsum  15734  sumss2  15740  fsumcvg2  15741  fsumclf  15752  fsumzcl2  15753  fsumsplitf  15756  sumsnf  15757  fsumsplit1  15759  sumsns  15764  fsummsnunz  15768  fsumsplitsnun  15769  fsum2dlem  15784  fsumcnv  15787  fsumcom2  15788  fsumshftm  15795  fsum0diag2  15797  fsum00  15812  fsumabs  15815  fsumrlim  15825  fsumo1  15826  o1fsum  15827  fsumiun  15835  infcvgaux1i  15871  prodeq2ii  15925  prodmolem3  15947  prodmolem2a  15948  zprod  15951  fprod  15955  fprodntriv  15956  prodss  15961  fprodser  15963  fprodcllemf  15972  prodsn  15976  prodsnf  15978  fprodm1s  15984  fprodp1s  15985  prodsns  15986  fprodabs  15988  fprodn0  15993  fprod2dlem  15994  fprodcnv  15997  fprodcom2  15998  fproddivf  16001  fprodsplitf  16002  fprodsplit1f  16004  fprodle  16010  fprodmodd  16011  fprodefsum  16109  sumeven  16404  sumodd  16405  pcmpt  16910  pcmptdvds  16912  natpropd  17990  fucpropd  17991  gsummpt1n0  19944  gsumcom2  19954  gsummptnn0fz  19965  dprd2d2  20025  psrass1lem  21890  mpfrcl  22041  coe1fzgsumdlem  22239  gsumply1eq  22245  evl1gsumdlem  22292  mdetralt2  22545  mdetunilem2  22549  madugsum  22579  fiuncmp  23340  ptcld  23549  ptcldmpt  23550  ptclsg  23551  elmptrab  23763  prdsdsf  24304  prdsxmet  24306  fsumcn  24810  fsum2cn  24811  ovolfiniun  25452  ovoliunlem3  25455  ovoliun  25456  ovoliun2  25457  ovoliunnul  25458  finiunmbl  25495  volfiniun  25498  iundisj  25499  iundisj2  25500  iunmbl  25504  iunmbl2  25508  itgss3  25766  itgfsum  25778  itgabs  25786  limciun  25845  dvmptfsum  25929  dvfsumle  25976  dvfsumleOLD  25977  dvfsumabs  25979  dvfsumlem1  25982  dvfsumlem2  25983  dvfsumlem2OLD  25984  dvfsumlem3  25985  dvfsumlem4  25986  dvfsumrlim  25988  dvfsumrlim2  25989  dvfsum2  25991  itgsubstlem  26005  itgsubst  26006  rlimcnp2  26926  fsumdvdscom  27145  fsumdvdsmul  27155  fsumdvdsmulOLD  27157  fsumvma  27174  dchrisumlema  27449  dchrisumlem2  27451  dchrisumlem3  27452  ifeqeqx  32469  iunxpssiun1  32495  disjorsf  32507  disjabrex  32509  disjabrexf  32510  iundisjf  32516  iundisj2f  32517  disjunsn  32521  suppss2f  32562  2ndresdju  32573  fmptdF  32580  fmptcof2  32581  acunirnmpt2f  32585  aciunf1lem  32586  funcnv4mpt  32593  f1od2  32644  iundisjfi  32719  iundisj2fi  32720  fsumiunle  32754  gsummpt2co  32988  gsumpart  32997  gsumvsca1  33169  gsumvsca2  33170  rmfsupp2  33179  esumpfinvalf  34053  esum2dlem  34069  esumiun  34071  fiunelros  34151  measiun  34195  voliune  34206  volfiniune  34207  sbcaltop  35945  weiunpo  36429  weiunso  36430  weiunfr  36431  weiunse  36432  bj-sbeqALT  36864  rdgssun  37342  finxpreclem2  37354  phpreu  37574  finixpnum  37575  ptrest  37589  poimirlem23  37613  poimirlem24  37614  poimirlem25  37615  poimirlem26  37616  poimirlem27  37617  poimirlem28  37618  mbfposadd  37637  itgabsnc  37659  ftc1cnnclem  37661  ftc2nc  37672  fsumshftd  38916  riotasv2s  38922  cdleme31sn  40345  cdleme31sn1  40346  cdleme31se2  40348  cdleme32fva  40402  cdleme42b  40443  hlhilset  41899  evl1gprodd  42076  idomnnzgmulnz  42092  deg1gprod  42099  fmpocos  42232  mzpsubst  42718  rabdiophlem2  42772  elnn0rabdioph  42773  dvdsrabdioph  42780  fphpd  42786  monotuz  42912  oddcomabszz  42915  aomclem6  43030  flcidc  43141  fsumcnf  44993  sumsnd  44998  fiiuncl  45037  eliin2f  45076  disjf1  45155  disjrnmpt2  45160  disjinfi  45164  fmptf  45211  fmptff  45241  iuneqfzuzlem  45309  supxrleubrnmptf  45426  fsummulc1f  45548  fsumnncl  45549  fsumf1of  45551  fsumiunss  45552  fsumreclf  45553  fsumlessf  45554  fsumsermpt  45556  fprodexp  45571  fprodabs2  45572  mccllem  45574  fprodcnlem  45576  fprodcn  45577  climsubmpt  45637  climeldmeqmpt  45645  climfveqmpt  45648  climfveqmpt3  45659  climeldmeqmpt3  45666  climinf2mpt  45691  climinfmpt  45692  limsupequzmptf  45708  fprodcncf  45877  dvmptmulf  45914  dvnmptdivc  45915  dvmptfprod  45922  iblsplitf  45947  fourierdlem86  46169  fourierdlem112  46195  sge0f1o  46359  sge0lempt  46387  sge0iunmptlemfi  46390  sge0iunmptlemre  46392  sge0iunmpt  46395  sge0ltfirpmpt2  46403  sge0isummpt2  46409  sge0xaddlem2  46411  sge0xadd  46412  meadjiun  46443  hoimbl2  46642  vonhoire  46649  vonn0ioo2  46667  vonn0icc2  46669  csbafv12g  47114  csbaovg  47157  csbafv212g  47196  fsummsndifre  47334  fsumsplitsndif  47335  fsummmodsndifre  47336  fsummmodsnunz  47337  dmmpossx2  48260