Theorem csbeq1a 3860

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-12 2213  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-sbc 3739  df-csb 3847

This theorem is used by:  csbhypf  3874  csbiebt  3875  cbvrabcsfw  3887  cbvralcsf  3888  cbvreucsf  3890  cbvrabcsf  3891  rspc2vd  3894  sbcnestgfw  4378  sbcnestgf  4383  csbun  4398  csbin  4399  csbdif  4480  csbif  4539  disjors  5085  invdisjrab  5089  disjxiun  5099  disjxun  5100  sbcbr123  5158  eusvnf  5353  reusv2lem4  5362  reusv2  5364  moop2  5471  iunopeqop  5490  iunopeqopOLD  5491  pofun  5573  opeliunxp  5714  opeliun2xp  5715  elrnmpt1  5938  resmptf  6029  csbima12  6069  csbcog  6289  fvmpt2f  6982  fvmpts  6985  fvmptdf  6988  fvmpt2i  6992  fvmptex  6996  fmptco  7118  fmptcof  7119  fmptcos  7120  elabrex  7234  elabrexg  7235  fliftfuns  7310  riotaeqimp  7391  csbov123  7452  ovmpos  7556  fvmpopr2d  7570  ofmpteq  7699  csbopeq1a  8044  mpomptsx  8058  dmmpossx  8060  fmpox  8061  el2mpocsbcl  8079  offval22  8082  ovmptss  8087  fmpoco  8089  mpoxeldm  8206  mpocurryd  8264  mpocurryvald  8265  fvmpocurryd  8266  eqerlem  8731  qliftfuns  8803  mptelixpg  8941  boxcutc  8947  xpf1o  9136  iunfi  9310  wdom2d  9552  ixpiunwdom  9562  hsmexlem2  10476  ac6c4  10530  iundom2g  10595  seqof2  14171  rlimcld2  15712  sumeq2ii  15827  summolem3  15847  summolem2a  15848  zsum  15851  fsum  15853  sumss2  15859  fsumcvg2  15860  fsumclf  15871  fsumzcl2  15872  fsumsplitf  15875  sumsnf  15876  fsumsplit1  15878  sumsns  15883  fsummsnunz  15887  fsumsplitsnun  15888  fsum2dlem  15903  fsumcnv  15906  fsumcom2  15907  fsumshftm  15914  fsum0diag2  15916  fsum00  15932  fsumabs  15935  fsumrlim  15945  fsumo1  15946  o1fsum  15947  fsumiun  15955  infcvgaux1i  15993  prodeq2ii  16047  prodmolem3  16067  prodmolem2a  16068  zprod  16071  fprod  16075  fprodntriv  16076  prodss  16081  fprodser  16083  fprodcllemf  16092  prodsn  16096  prodsnf  16098  fprodm1s  16104  fprodp1s  16105  prodsns  16106  fprodabs  16108  fprodn0  16113  fprod2dlem  16114  fprodcnv  16117  fprodcom2  16118  fproddivf  16121  fprodsplitf  16122  fprodsplit1f  16124  fprodle  16130  fprodmodd  16131  fprodefsum  16228  sumeven  16524  sumodd  16525  pcmpt  17031  pcmptdvds  17033  natpropd  18115  fucpropd  18116  gsummpt1n0  20140  gsumcom2  20150  gsummptnn0fz  20161  dprd2d2  20221  psrass1lem  22202  mpfrcl  22355  coe1fzgsumdlem  22582  gsumply1eq  22588  evl1gsumdlem  22635  mdetralt2  22885  mdetunilem2  22889  madugsum  22919  fiuncmp  23683  ptcld  23893  ptcldmpt  23894  ptclsg  23895  elmptrab  24107  prdsdsf  24647  prdsxmet  24649  fsumcn  25152  fsum2cn  25153  ovolfiniun  25783  ovoliunlem3  25786  ovoliun  25787  ovoliun2  25788  ovoliunnul  25789  finiunmbl  25826  volfiniun  25829  iundisj  25830  iundisj2  25831  iunmbl  25835  iunmbl2  25839  itgss3  26096  itgfsum  26108  itgabs  26116  limciun  26175  dvmptfsum  26256  dvfsumle  26302  dvfsumabs  26304  dvfsumlem1  26307  dvfsumlem2  26308  dvfsumlem3  26309  dvfsumlem4  26310  dvfsumrlim  26312  dvfsumrlim2  26313  dvfsum2  26315  itgsubstlem  26329  itgsubst  26330  rlimcnp2  27257  fsumdvdscom  27475  fsumdvdsmul  27485  fsumvma  27503  dchrisumlema  27778  dchrisumlem2  27780  dchrisumlem3  27781  ifeqeqx  33071  iunxpssiun1  33095  disjorsf  33107  disjabrex  33109  disjabrexf  33110  iundisjf  33116  iundisj2f  33117  disjunsn  33121  suppss2f  33165  2ndresdju  33176  fmptdf2  33183  fmptcof2  33184  acunirnmpt2f  33188  aciunf1lem  33189  funcnv4mpt  33195  f1od2  33244  iundisjfi  33321  iundisj2fi  33322  fsumiunle  33353  gsummpt2co  33542  gsummptp1  33551  gsumpart  33557  gsumvsca1  33720  gsumvsca2  33721  rmfsupp2  33731  esumpfinvalf  34641  esum2dlem  34657  esumiun  34659  fiunelros  34740  measiun  34784  voliune  34795  volfiniune  34796  sbcaltop  36668  weiunpo  37175  weiunso  37176  weiunfr  37177  weiunse  37178  csbttc  37219  bj-sbeqALT  37734  rdgssun  38221  finxpreclem2  38233  phpreu  38447  finixpnum  38448  ptrest  38457  poimirlem23  38481  poimirlem24  38482  poimirlem25  38483  poimirlem26  38484  poimirlem27  38485  poimirlem28  38486  mbfposadd  38505  itgabsnc  38527  ftc1cnnclem  38529  ftc2nc  38540  fsumshftd  39929  riotasv2s  39935  cdleme31sn  41357  cdleme31sn1  41358  cdleme31se2  41360  cdleme32fva  41414  cdleme42b  41455  hlhilset  42911  evl1gprodd  43087  idomnnzgmulnz  43103  deg1gprod  43110  fmpocos  43207  mzpsubst  43697  rabdiophlem2  43747  elnn0rabdioph  43748  dvdsrabdioph  43755  fphpd  43761  monotuz  43886  oddcomabszz  43889  aomclem6  44004  flcidc  44115  fsumcnf  45959  sumsnd  45964  fiiuncl  46003  eliin2f  46040  disjf1  46119  disjrnmpt2  46124  disjinfi  46128  fmptf  46172  fmptff  46202  iuneqfzuzlem  46268  supxrleubrnmptf  46383  fsummulc1f  46505  fsumnncl  46506  fsumf1of  46508  fsumiunss  46509  fsumreclf  46510  fsumlessf  46511  fsumsermpt  46513  fprodexp  46528  fprodabs2  46529  mccllem  46531  fprodcnlem  46533  fprodcn  46534  climsubmpt  46592  climeldmeqmpt  46600  climfveqmpt  46603  climfveqmpt3  46614  climeldmeqmpt3  46621  climinf2mpt  46646  climinfmpt  46647  limsupequzmptf  46663  fprodcncf  46832  dvmptmulf  46869  dvnmptdivc  46870  dvmptfprod  46877  iblsplitf  46902  fourierdlem86  47124  fourierdlem112  47150  sge0f1o  47314  sge0lempt  47342  sge0iunmptlemfi  47345  sge0iunmptlemre  47347  sge0iunmpt  47350  sge0ltfirpmpt2  47358  sge0isummpt2  47364  sge0xaddlem2  47366  sge0xadd  47367  meadjiun  47398  hoimbl2  47597  vonhoire  47604  vonn0ioo2  47622  vonn0icc2  47624  csbafv12g  48129  csbaovg  48172  csbafv212g  48211  fsummsndifre  48372  fsumsplitsndif  48373  fsummmodsndifre  48374  fsummmodsnunz  48375  dmmpossx2  49371