Theorem csbeq1a 3865

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ⦋csb 3851

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-12 2216  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-sbc 3743  df-csb 3852

This theorem is used by:  csbhypf  3879  csbiebt  3880  cbvrabcsfw  3892  cbvralcsf  3893  cbvreucsf  3895  cbvrabcsf  3896  rspc2vd  3899  sbcnestgfw  4382  sbcnestgf  4387  csbun  4402  csbin  4403  csbdif  4484  csbif  4543  disjors  5089  invdisjrab  5093  disjxiun  5103  disjxun  5104  sbcbr123  5163  eusvnf  5358  reusv2lem4  5367  reusv2  5369  moop2  5478  iunopeqop  5498  iunopeqopOLD  5499  pofun  5581  opeliunxp  5722  opeliun2xp  5723  elrnmpt1  5949  resmptf  6043  csbima12  6088  csbcog  6318  fvmpt2f  7017  fvmpts  7020  fvmptdf  7023  fvmpt2i  7027  fvmptex  7031  fmptco  7154  fmptcof  7155  fmptcos  7156  elabrex  7269  elabrexg  7270  fliftfuns  7345  riotaeqimp  7426  csbov123  7487  ovmpos  7592  fvmpopr2d  7606  ofmpteq  7740  csbopeq1a  8086  mpomptsx  8100  dmmpossx  8102  fmpox  8103  el2mpocsbcl  8121  offval22  8124  ovmptssOLD  8130  fmpoco  8132  f1od2  8135  mpoxeldm  8256  mpocurryd  8314  mpocurryvald  8315  fvmpocurryd  8316  eqerlem  8781  qliftfuns  8853  mptelixpg  8991  boxcutc  8997  xpf1o  9186  iunfi  9360  wdom2d  9601  ixpiunwdom  9611  hsmexlem2  10532  ac6c4  10586  iundom2g  10651  seqof2  14230  rlimcld2  15774  sumeq2ii  15889  summolem3  15909  summolem2a  15910  zsum  15913  fsum  15915  sumss2  15921  fsumcvg2  15922  fsumclf  15933  fsumzcl2  15934  fsumsplitf  15937  sumsnf  15938  fsumsplit1  15940  sumsns  15945  fsummsnunz  15949  fsumsplitsnun  15950  fsum2dlem  15965  fsumcnv  15968  fsumcom2  15969  fsumshftm  15976  fsum0diag2  15978  fsum00  15994  fsumabs  15997  fsumrlim  16007  fsumo1  16008  o1fsum  16009  fsumiun  16017  infcvgaux1i  16055  prodeq2ii  16109  prodmolem3  16129  prodmolem2a  16130  zprod  16133  fprod  16137  fprodntriv  16138  prodss  16143  fprodser  16145  fprodcllemf  16154  prodsn  16158  prodsnf  16160  fprodm1s  16166  fprodp1s  16167  prodsns  16168  fprodabs  16170  fprodn0  16175  fprod2dlem  16176  fprodcnv  16179  fprodcom2  16180  fproddivf  16183  fprodsplitf  16184  fprodsplit1f  16186  fprodle  16192  fprodmodd  16193  fprodefsum  16290  sumeven  16586  sumodd  16587  pcmpt  17099  pcmptdvds  17101  natpropd  18183  fucpropd  18184  gsummpt1n0  20209  gsumcom2  20219  gsummptnn0fz  20230  dprd2d2  20290  psrass1lem  22271  mpfrcl  22424  coe1fzgsumdlem  22651  gsumply1eq  22657  evl1gsumdlem  22704  mdetralt2  22954  mdetunilem2  22958  madugsum  22988  fiuncmp  23752  ptcld  23962  ptcldmpt  23963  ptclsg  23964  elmptrab  24176  prdsdsf  24716  prdsxmet  24718  fsumcn  25221  fsum2cn  25222  ovolfiniun  25852  ovoliunlem3  25855  ovoliun  25856  ovoliun2  25857  ovoliunnul  25858  finiunmbl  25895  volfiniun  25898  iundisj  25899  iundisj2  25900  iunmbl  25904  iunmbl2  25908  itgss3  26165  itgfsum  26177  itgabs  26185  limciun  26244  dvmptfsum  26325  dvfsumle  26371  dvfsumabs  26373  dvfsumlem1  26376  dvfsumlem2  26377  dvfsumlem3  26378  dvfsumlem4  26379  dvfsumrlim  26381  dvfsumrlim2  26382  dvfsum2  26384  itgsubstlem  26398  itgsubst  26399  rlimcnp2  27324  fsumdvdscom  27542  fsumdvdsmul  27552  fsumvma  27570  dchrisumlema  27845  dchrisumlem2  27847  dchrisumlem3  27848  ifeqeqx  33210  iunxpssiun1  33234  disjorsf  33246  disjabrex  33248  disjabrexf  33249  iundisjf  33255  iundisj2f  33256  disjunsn  33260  suppss2f  33304  2ndresdju  33315  fmptdf2  33322  fmptcof2  33323  acunirnmpt2f  33327  aciunf1lem  33328  funcnv4mpt  33334  iundisjfi  33458  iundisj2fi  33459  fsumiunle  33490  gsummpt2co  33679  gsummptp1  33688  gsumpart  33694  gsumvsca1  33857  gsumvsca2  33858  rmfsupp2  33868  esumpfinvalf  34778  esum2dlem  34794  esumiun  34796  fiunelros  34877  measiun  34921  voliune  34932  volfiniune  34933  sbcaltop  36924  weiunpo  37431  weiunso  37432  weiunfr  37433  weiunse  37434  csbttc  37475  bj-sbeqALT  37990  rdgssun  38493  finxpreclem2  38505  phpreu  38719  finixpnum  38720  ptrest  38729  poimirlem23  38753  poimirlem24  38754  poimirlem25  38755  poimirlem26  38756  poimirlem27  38757  poimirlem28  38758  mbfposadd  38777  itgabsnc  38799  ftc1cnnclem  38801  ftc2nc  38812  fsumshftd  40201  riotasv2s  40207  cdleme31sn  41629  cdleme31sn1  41630  cdleme31se2  41632  cdleme32fva  41686  cdleme42b  41727  hlhilset  43183  evl1gprodd  43359  idomnnzgmulnz  43375  deg1gprod  43382  fmpocos  43480  mzpsubst  43952  rabdiophlem2  44002  elnn0rabdioph  44003  dvdsrabdioph  44010  fphpd  44016  monotuz  44141  oddcomabszz  44144  aomclem6  44254  flcidc  44364  fsumcnf  46243  sumsnd  46248  fiiuncl  46287  eliin2f  46324  disjf1  46403  disjrnmpt2  46408  disjinfi  46412  fmptf  46456  fmptff  46486  iuneqfzuzlem  46551  supxrleubrnmptf  46666  fsummulc1f  46788  fsumnncl  46789  fsumf1of  46791  fsumiunss  46792  fsumreclf  46793  fsumlessf  46794  fsumsermpt  46796  fprodexp  46811  fprodabs2  46812  mccllem  46814  fprodcnlem  46816  fprodcn  46817  climsubmpt  46875  climeldmeqmpt  46883  climfveqmpt  46886  climfveqmpt3  46897  climeldmeqmpt3  46904  climinf2mpt  46929  climinfmpt  46930  limsupequzmptf  46946  fprodcncf  47115  dvmptmulf  47152  dvnmptdivc  47153  dvmptfprod  47160  iblsplitf  47185  fourierdlem86  47407  fourierdlem112  47433  sge0f1o  47597  sge0lempt  47625  sge0iunmptlemfi  47628  sge0iunmptlemre  47630  sge0iunmpt  47633  sge0ltfirpmpt2  47641  sge0isummpt2  47647  sge0xaddlem2  47649  sge0xadd  47650  meadjiun  47681  hoimbl2  47880  vonhoire  47887  vonn0ioo2  47905  vonn0icc2  47907  csbafv12g  48412  csbaovg  48455  csbafv212g  48494  fsummsndifre  48655  fsumsplitsndif  48656  fsummmodsndifre  48657  fsummmodsnunz  48658  dmmpossx2  49654