Theorem csbeq1a 3866

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

Syntax hints:   → wi 4   = wceq 1568  ⦋csb 3852

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-12 2211  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1571  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-sbc 3744  df-csb 3853

This theorem is referenced by:  csbhypf  3880  csbiebt  3881  cbvrabcsfw  3893  cbvralcsf  3894  cbvreucsf  3896  cbvrabcsf  3897  rspc2vd  3900  sbcnestgfw  4385  sbcnestgf  4390  csbun  4405  csbin  4406  csbdif  4485  csbif  4544  disjors  5091  invdisjrab  5095  disjxiun  5105  disjxun  5106  sbcbr123  5164  eusvnf  5363  reusv2lem4  5372  reusv2  5374  moop2  5485  iunopeqop  5504  iunopeqopOLD  5505  pofun  5587  opeliunxp  5728  opeliun2xp  5729  elrnmpt1  5950  resmptf  6041  csbima12  6081  csbcog  6298  fvmpt2f  6990  fvmpts  6993  fvmptdf  6996  fvmpt2i  7000  fvmptex  7004  fmptco  7125  fmptcof  7126  fmptcos  7127  elabrex  7240  elabrexg  7241  fliftfuns  7312  riotaeqimp  7393  csbov123  7454  ovmpos  7558  fvmpopr2d  7572  ofmpteq  7697  csbopeq1a  8046  mpomptsx  8060  dmmpossx  8062  fmpox  8063  el2mpocsbcl  8079  offval22  8082  ovmptss  8087  fmpoco  8089  mpoxeldm  8206  mpocurryd  8264  mpocurryvald  8265  fvmpocurryd  8266  eqerlem  8729  qliftfuns  8801  mptelixpg  8932  boxcutc  8938  xpf1o  9126  iunfi  9299  wdom2d  9541  ixpiunwdom  9551  hsmexlem2  10410  ac6c4  10464  iundom2g  10523  seqof2  14095  rlimcld2  15628  sumeq2ii  15743  summolem3  15764  summolem2a  15765  zsum  15768  fsum  15770  sumss2  15776  fsumcvg2  15777  fsumclf  15788  fsumzcl2  15789  fsumsplitf  15792  sumsnf  15793  fsumsplit1  15795  sumsns  15800  fsummsnunz  15804  fsumsplitsnun  15805  fsum2dlem  15820  fsumcnv  15823  fsumcom2  15824  fsumshftm  15831  fsum0diag2  15833  fsum00  15849  fsumabs  15852  fsumrlim  15862  fsumo1  15863  o1fsum  15864  fsumiun  15872  infcvgaux1i  15910  prodeq2ii  15964  prodmolem3  15986  prodmolem2a  15987  zprod  15990  fprod  15994  fprodntriv  15995  prodss  16000  fprodser  16002  fprodcllemf  16011  prodsn  16015  prodsnf  16017  fprodm1s  16023  fprodp1s  16024  prodsns  16025  fprodabs  16027  fprodn0  16032  fprod2dlem  16033  fprodcnv  16036  fprodcom2  16037  fproddivf  16040  fprodsplitf  16041  fprodsplit1f  16043  fprodle  16049  fprodmodd  16050  fprodefsum  16148  sumeven  16444  sumodd  16445  pcmpt  16951  pcmptdvds  16953  natpropd  18035  fucpropd  18036  gsummpt1n0  20034  gsumcom2  20044  gsummptnn0fz  20055  dprd2d2  20115  psrass1lem  22062  mpfrcl  22215  coe1fzgsumdlem  22442  gsumply1eq  22448  evl1gsumdlem  22495  mdetralt2  22745  mdetunilem2  22749  madugsum  22779  fiuncmp  23540  ptcld  23749  ptcldmpt  23750  ptclsg  23751  elmptrab  23963  prdsdsf  24503  prdsxmet  24505  fsumcn  25008  fsum2cn  25009  ovolfiniun  25639  ovoliunlem3  25642  ovoliun  25643  ovoliun2  25644  ovoliunnul  25645  finiunmbl  25682  volfiniun  25685  iundisj  25686  iundisj2  25687  iunmbl  25691  iunmbl2  25695  itgss3  25953  itgfsum  25965  itgabs  25973  limciun  26032  dvmptfsum  26113  dvfsumle  26159  dvfsumabs  26161  dvfsumlem1  26164  dvfsumlem2  26165  dvfsumlem3  26166  dvfsumlem4  26167  dvfsumrlim  26169  dvfsumrlim2  26170  dvfsum2  26172  itgsubstlem  26186  itgsubst  26187  rlimcnp2  27107  fsumdvdscom  27325  fsumdvdsmul  27335  fsumvma  27353  dchrisumlema  27628  dchrisumlem2  27630  dchrisumlem3  27631  ifeqeqx  32854  iunxpssiun1  32879  disjorsf  32891  disjabrex  32893  disjabrexf  32894  iundisjf  32900  iundisj2f  32901  disjunsn  32905  suppss2f  32949  2ndresdju  32960  fmptdF  32967  fmptcof2  32968  acunirnmpt2f  32972  aciunf1lem  32973  funcnv4mpt  32979  f1od2  33030  iundisjfi  33107  iundisj2fi  33108  fsumiunle  33139  gsummpt2co  33334  gsummptp1  33343  gsumpart  33349  gsumvsca1  33512  gsumvsca2  33513  rmfsupp2  33523  esumpfinvalf  34432  esum2dlem  34448  esumiun  34450  fiunelros  34530  measiun  34574  voliune  34585  volfiniune  34586  sbcaltop  36427  weiunpo  36920  weiunso  36921  weiunfr  36922  weiunse  36923  csbttc  36964  bj-sbeqALT  37479  rdgssun  37968  finxpreclem2  37980  phpreu  38199  finixpnum  38200  ptrest  38214  poimirlem23  38238  poimirlem24  38239  poimirlem25  38240  poimirlem26  38241  poimirlem27  38242  poimirlem28  38243  mbfposadd  38262  itgabsnc  38284  ftc1cnnclem  38286  ftc2nc  38297  fsumshftd  39672  riotasv2s  39678  cdleme31sn  41100  cdleme31sn1  41101  cdleme31se2  41103  cdleme32fva  41157  cdleme42b  41198  hlhilset  42654  evl1gprodd  42830  idomnnzgmulnz  42846  deg1gprod  42853  fmpocos  42950  mzpsubst  43427  rabdiophlem2  43477  elnn0rabdioph  43478  dvdsrabdioph  43485  fphpd  43491  monotuz  43616  oddcomabszz  43619  aomclem6  43734  flcidc  43845  fsumcnf  45689  sumsnd  45694  fiiuncl  45733  eliin2f  45770  disjf1  45849  disjrnmpt2  45854  disjinfi  45858  fmptf  45902  fmptff  45932  iuneqfzuzlem  45998  supxrleubrnmptf  46113  fsummulc1f  46235  fsumnncl  46236  fsumf1of  46238  fsumiunss  46239  fsumreclf  46240  fsumlessf  46241  fsumsermpt  46243  fprodexp  46258  fprodabs2  46259  mccllem  46261  fprodcnlem  46263  fprodcn  46264  climsubmpt  46322  climeldmeqmpt  46330  climfveqmpt  46333  climfveqmpt3  46344  climeldmeqmpt3  46351  climinf2mpt  46376  climinfmpt  46377  limsupequzmptf  46393  fprodcncf  46562  dvmptmulf  46599  dvnmptdivc  46600  dvmptfprod  46607  iblsplitf  46632  fourierdlem86  46854  fourierdlem112  46880  sge0f1o  47044  sge0lempt  47072  sge0iunmptlemfi  47075  sge0iunmptlemre  47077  sge0iunmpt  47080  sge0ltfirpmpt2  47088  sge0isummpt2  47094  sge0xaddlem2  47096  sge0xadd  47097  meadjiun  47128  hoimbl2  47327  vonhoire  47334  vonn0ioo2  47352  vonn0icc2  47354  csbafv12g  47819  csbaovg  47862  csbafv212g  47901  fsummsndifre  48062  fsumsplitsndif  48063  fsummmodsndifre  48064  fsummmodsnunz  48065  dmmpossx2  49062