Theorem csbeq1a 3908

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

Syntax hints:   → wi 4   = wceq 1542  ⦋csb 3894

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-12 2172  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-sbc 3779  df-csb 3895

This theorem is referenced by:  csbhypf  3923  csbiebt  3924  cbvrabcsfw  3938  cbvralcsf  3939  cbvreucsf  3941  cbvrabcsf  3942  rspc2vd  3945  sbcnestgfw  4419  sbcnestgf  4424  csbun  4439  csbin  4440  csbdif  4528  csbif  4586  disjors  5130  invdisjrabw  5134  invdisjrab  5135  disjxiun  5146  disjxun  5147  sbcbr123  5203  eusvnf  5391  reusv2lem4  5400  reusv2  5402  moop2  5503  iunopeqop  5522  pofun  5607  opeliunxp  5744  elrnmpt1  5958  resmptf  6040  csbima12  6079  csbcog  6297  fvmpt2f  7000  fvmpts  7002  fvmptdf  7005  fvmpt2i  7009  fvmptex  7013  fmptco  7127  fmptcof  7128  fmptcos  7129  elabrex  7242  fliftfuns  7311  riotaeqimp  7392  csbov123  7451  ovmpos  7556  fvmpopr2d  7569  ofmpteq  7692  csbopeq1a  8036  mpomptsx  8050  dmmpossx  8052  fmpox  8053  el2mpocsbcl  8071  offval22  8074  ovmptss  8079  fmpoco  8081  mpoxeldm  8196  mpocurryd  8254  mpocurryvald  8255  fvmpocurryd  8256  eqerlem  8737  qliftfuns  8798  mptelixpg  8929  boxcutc  8935  xpf1o  9139  iunfi  9340  wdom2d  9575  ixpiunwdom  9585  hsmexlem2  10422  ac6c4  10476  iundom2g  10535  seqof2  14026  rlimcld2  15522  sumeq2ii  15639  summolem3  15660  summolem2a  15661  zsum  15664  fsum  15666  sumss2  15672  fsumcvg2  15673  fsumclf  15684  fsumzcl2  15685  fsumsplitf  15688  sumsnf  15689  fsumsplit1  15691  sumsns  15696  fsummsnunz  15700  fsumsplitsnun  15701  fsum2dlem  15716  fsumcnv  15719  fsumcom2  15720  fsumshftm  15727  fsum0diag2  15729  fsum00  15744  fsumabs  15747  fsumrlim  15757  fsumo1  15758  o1fsum  15759  fsumiun  15767  infcvgaux1i  15803  prodeq2ii  15857  prodmolem3  15877  prodmolem2a  15878  zprod  15881  fprod  15885  fprodntriv  15886  prodss  15891  fprodser  15893  fprodcllemf  15902  prodsn  15906  prodsnf  15908  fprodm1s  15914  fprodp1s  15915  prodsns  15916  fprodabs  15918  fprodn0  15923  fprod2dlem  15924  fprodcnv  15927  fprodcom2  15928  fproddivf  15931  fprodsplitf  15932  fprodsplit1f  15934  fprodle  15940  fprodmodd  15941  fprodefsum  16038  sumeven  16330  sumodd  16331  pcmpt  16825  pcmptdvds  16827  natpropd  17929  fucpropd  17930  gsummpt1n0  19833  gsumcom2  19843  gsummptnn0fz  19854  dprd2d2  19914  psrass1lemOLD  21493  psrass1lem  21496  mpfrcl  21648  coe1fzgsumdlem  21825  gsumply1eq  21829  evl1gsumdlem  21875  mdetralt2  22111  mdetunilem2  22115  madugsum  22145  fiuncmp  22908  ptcld  23117  ptcldmpt  23118  ptclsg  23119  elmptrab  23331  prdsdsf  23873  prdsxmet  23875  fsumcn  24386  fsum2cn  24387  ovolfiniun  25018  ovoliunlem3  25021  ovoliun  25022  ovoliun2  25023  ovoliunnul  25024  finiunmbl  25061  volfiniun  25064  iundisj  25065  iundisj2  25066  iunmbl  25070  iunmbl2  25074  itgss3  25332  itgfsum  25344  itgabs  25352  limciun  25411  dvmptfsum  25492  dvfsumle  25538  dvfsumabs  25540  dvfsumlem1  25543  dvfsumlem2  25544  dvfsumlem3  25545  dvfsumlem4  25546  dvfsumrlim  25548  dvfsumrlim2  25549  dvfsum2  25551  itgsubstlem  25565  itgsubst  25566  rlimcnp2  26471  fsumdvdscom  26689  fsumdvdsmul  26699  fsumvma  26716  dchrisumlema  26991  dchrisumlem2  26993  dchrisumlem3  26994  ifeqeqx  31774  disjorsf  31811  disjabrex  31813  disjabrexf  31814  iundisjf  31820  iundisj2f  31821  disjunsn  31825  suppss2f  31863  2ndresdju  31874  fmptdF  31881  fmptcof2  31882  acunirnmpt2f  31886  aciunf1lem  31887  funcnv4mpt  31894  f1od2  31946  iundisjfi  32007  iundisj2fi  32008  fsumiunle  32035  gsummpt2co  32200  gsumpart  32207  gsumvsca1  32371  gsumvsca2  32372  rmfsupp2  32387  esumpfinvalf  33074  esum2dlem  33090  esumiun  33092  fiunelros  33172  measiun  33216  voliune  33227  volfiniune  33228  sbcaltop  34953  gg-dvfsumle  35182  gg-dvfsumlem2  35183  bj-sbeqALT  35780  rdgssun  36259  finxpreclem2  36271  phpreu  36472  finixpnum  36473  ptrest  36487  poimirlem23  36511  poimirlem24  36512  poimirlem25  36513  poimirlem26  36514  poimirlem27  36515  poimirlem28  36516  mbfposadd  36535  itgabsnc  36557  ftc1cnnclem  36559  ftc2nc  36570  fsumshftd  37822  riotasv2s  37828  cdleme31sn  39251  cdleme31sn1  39252  cdleme31se2  39254  cdleme32fva  39308  cdleme42b  39349  hlhilset  40805  fmpocos  41056  mzpsubst  41486  rabdiophlem2  41540  elnn0rabdioph  41541  dvdsrabdioph  41548  fphpd  41554  monotuz  41680  oddcomabszz  41683  aomclem6  41801  flcidc  41916  fsumcnf  43705  sumsnd  43710  elabrexg  43728  fiiuncl  43752  eliin2f  43793  disjf1  43880  disjrnmpt2  43886  disjinfi  43891  fmptf  43942  fmptff  43974  iuneqfzuzlem  44044  supxrleubrnmptf  44161  fsummulc1f  44287  fsumnncl  44288  fsumf1of  44290  fsumiunss  44291  fsumreclf  44292  fsumlessf  44293  fsumsermpt  44295  fprodexp  44310  fprodabs2  44311  mccllem  44313  fprodcnlem  44315  fprodcn  44316  climsubmpt  44376  climeldmeqmpt  44384  climfveqmpt  44387  climfveqmpt3  44398  climeldmeqmpt3  44405  climinf2mpt  44430  climinfmpt  44431  limsupequzmptf  44447  fprodcncf  44616  dvmptmulf  44653  dvnmptdivc  44654  dvmptfprod  44661  iblsplitf  44686  fourierdlem86  44908  fourierdlem112  44934  sge0f1o  45098  sge0lempt  45126  sge0iunmptlemfi  45129  sge0iunmptlemre  45131  sge0iunmpt  45134  sge0ltfirpmpt2  45142  sge0isummpt2  45148  sge0xaddlem2  45150  sge0xadd  45151  meadjiun  45182  hoimbl2  45381  vonhoire  45388  vonn0ioo2  45406  vonn0icc2  45408  csbafv12g  45845  csbaovg  45888  csbafv212g  45927  fsummsndifre  46040  fsumsplitsndif  46041  fsummmodsndifre  46042  fsummmodsnunz  46043  opeliun2xp  47008  dmmpossx2  47012