Theorem csbeq1a 3852

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-sbc 3730  df-csb 3839

This theorem is referenced by:  csbhypf  3866  csbiebt  3867  cbvrabcsfw  3879  cbvralcsf  3880  cbvreucsf  3882  cbvrabcsf  3883  rspc2vd  3886  sbcnestgfw  4362  sbcnestgf  4367  csbun  4382  csbin  4383  csbdif  4466  csbif  4525  disjors  5069  invdisjrab  5073  disjxiun  5083  disjxun  5084  sbcbr123  5140  eusvnf  5327  reusv2lem4  5336  reusv2  5338  moop2  5448  iunopeqop  5467  pofun  5548  opeliunxp  5689  opeliun2xp  5690  elrnmpt1  5907  resmptf  5996  csbima12  6036  csbcog  6253  fvmpt2f  6940  fvmpts  6943  fvmptdf  6946  fvmpt2i  6950  fvmptex  6954  fmptco  7074  fmptcof  7075  fmptcos  7076  elabrex  7188  elabrexg  7189  fliftfuns  7260  riotaeqimp  7341  csbov123  7402  ovmpos  7506  fvmpopr2d  7520  ofmpteq  7645  csbopeq1a  7994  mpomptsx  8008  dmmpossx  8010  fmpox  8011  el2mpocsbcl  8026  offval22  8029  ovmptss  8034  fmpoco  8036  mpoxeldm  8152  mpocurryd  8210  mpocurryvald  8211  fvmpocurryd  8212  eqerlem  8670  qliftfuns  8742  mptelixpg  8874  boxcutc  8880  xpf1o  9068  iunfi  9244  wdom2d  9486  ixpiunwdom  9496  hsmexlem2  10338  ac6c4  10392  iundom2g  10451  seqof2  13984  rlimcld2  15502  sumeq2ii  15617  summolem3  15638  summolem2a  15639  zsum  15642  fsum  15644  sumss2  15650  fsumcvg2  15651  fsumclf  15662  fsumzcl2  15663  fsumsplitf  15666  sumsnf  15667  fsumsplit1  15669  sumsns  15674  fsummsnunz  15678  fsumsplitsnun  15679  fsum2dlem  15694  fsumcnv  15697  fsumcom2  15698  fsumshftm  15705  fsum0diag2  15707  fsum00  15722  fsumabs  15725  fsumrlim  15735  fsumo1  15736  o1fsum  15737  fsumiun  15745  infcvgaux1i  15781  prodeq2ii  15835  prodmolem3  15857  prodmolem2a  15858  zprod  15861  fprod  15865  fprodntriv  15866  prodss  15871  fprodser  15873  fprodcllemf  15882  prodsn  15886  prodsnf  15888  fprodm1s  15894  fprodp1s  15895  prodsns  15896  fprodabs  15898  fprodn0  15903  fprod2dlem  15904  fprodcnv  15907  fprodcom2  15908  fproddivf  15911  fprodsplitf  15912  fprodsplit1f  15914  fprodle  15920  fprodmodd  15921  fprodefsum  16019  sumeven  16315  sumodd  16316  pcmpt  16821  pcmptdvds  16823  natpropd  17904  fucpropd  17905  gsummpt1n0  19898  gsumcom2  19908  gsummptnn0fz  19919  dprd2d2  19979  psrass1lem  21889  mpfrcl  22041  coe1fzgsumdlem  22246  gsumply1eq  22252  evl1gsumdlem  22299  mdetralt2  22552  mdetunilem2  22556  madugsum  22586  fiuncmp  23347  ptcld  23556  ptcldmpt  23557  ptclsg  23558  elmptrab  23770  prdsdsf  24310  prdsxmet  24312  fsumcn  24815  fsum2cn  24816  ovolfiniun  25446  ovoliunlem3  25449  ovoliun  25450  ovoliun2  25451  ovoliunnul  25452  finiunmbl  25489  volfiniun  25492  iundisj  25493  iundisj2  25494  iunmbl  25498  iunmbl2  25502  itgss3  25760  itgfsum  25772  itgabs  25780  limciun  25839  dvmptfsum  25920  dvfsumle  25967  dvfsumleOLD  25968  dvfsumabs  25970  dvfsumlem1  25973  dvfsumlem2  25974  dvfsumlem2OLD  25975  dvfsumlem3  25976  dvfsumlem4  25977  dvfsumrlim  25979  dvfsumrlim2  25980  dvfsum2  25982  itgsubstlem  25996  itgsubst  25997  rlimcnp2  26916  fsumdvdscom  27135  fsumdvdsmul  27145  fsumdvdsmulOLD  27147  fsumvma  27164  dchrisumlema  27439  dchrisumlem2  27441  dchrisumlem3  27442  ifeqeqx  32601  iunxpssiun1  32627  disjorsf  32639  disjabrex  32641  disjabrexf  32642  iundisjf  32648  iundisj2f  32649  disjunsn  32653  suppss2f  32700  2ndresdju  32711  fmptdF  32718  fmptcof2  32719  acunirnmpt2f  32723  aciunf1lem  32724  funcnv4mpt  32730  f1od2  32781  iundisjfi  32859  iundisj2fi  32860  fsumiunle  32893  gsummpt2co  33114  gsummptp1  33123  gsumpart  33129  gsumvsca1  33292  gsumvsca2  33293  rmfsupp2  33304  esumpfinvalf  34226  esum2dlem  34242  esumiun  34244  fiunelros  34324  measiun  34368  voliune  34379  volfiniune  34380  sbcaltop  36169  weiunpo  36653  weiunso  36654  weiunfr  36655  weiunse  36656  csbttc  36697  bj-sbeqALT  37205  rdgssun  37690  finxpreclem2  37702  phpreu  37916  finixpnum  37917  ptrest  37931  poimirlem23  37955  poimirlem24  37956  poimirlem25  37957  poimirlem26  37958  poimirlem27  37959  poimirlem28  37960  mbfposadd  37979  itgabsnc  38001  ftc1cnnclem  38003  ftc2nc  38014  fsumshftd  39389  riotasv2s  39395  cdleme31sn  40817  cdleme31sn1  40818  cdleme31se2  40820  cdleme32fva  40874  cdleme42b  40915  hlhilset  42371  evl1gprodd  42548  idomnnzgmulnz  42564  deg1gprod  42571  fmpocos  42667  mzpsubst  43179  rabdiophlem2  43233  elnn0rabdioph  43234  dvdsrabdioph  43241  fphpd  43247  monotuz  43372  oddcomabszz  43375  aomclem6  43490  flcidc  43601  fsumcnf  45455  sumsnd  45460  fiiuncl  45499  eliin2f  45537  disjf1  45616  disjrnmpt2  45621  disjinfi  45625  fmptf  45671  fmptff  45701  iuneqfzuzlem  45767  supxrleubrnmptf  45883  fsummulc1f  46005  fsumnncl  46006  fsumf1of  46008  fsumiunss  46009  fsumreclf  46010  fsumlessf  46011  fsumsermpt  46013  fprodexp  46028  fprodabs2  46029  mccllem  46031  fprodcnlem  46033  fprodcn  46034  climsubmpt  46092  climeldmeqmpt  46100  climfveqmpt  46103  climfveqmpt3  46114  climeldmeqmpt3  46121  climinf2mpt  46146  climinfmpt  46147  limsupequzmptf  46163  fprodcncf  46332  dvmptmulf  46369  dvnmptdivc  46370  dvmptfprod  46377  iblsplitf  46402  fourierdlem86  46624  fourierdlem112  46650  sge0f1o  46814  sge0lempt  46842  sge0iunmptlemfi  46845  sge0iunmptlemre  46847  sge0iunmpt  46850  sge0ltfirpmpt2  46858  sge0isummpt2  46864  sge0xaddlem2  46866  sge0xadd  46867  meadjiun  46898  hoimbl2  47097  vonhoire  47104  vonn0ioo2  47122  vonn0icc2  47124  csbafv12g  47571  csbaovg  47614  csbafv212g  47653  fsummsndifre  47806  fsumsplitsndif  47807  fsummmodsndifre  47808  fsummmodsnunz  47809  dmmpossx2  48771