Theorem csbeq1a 3862

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

Syntax hints:   → wi 4   = wceq 1541  ⦋csb 3848

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-12 2179  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-sbc 3740  df-csb 3849

This theorem is referenced by:  csbhypf  3876  csbiebt  3877  cbvrabcsfw  3889  cbvralcsf  3890  cbvreucsf  3892  cbvrabcsf  3893  rspc2vd  3896  sbcnestgfw  4369  sbcnestgf  4374  csbun  4389  csbin  4390  csbdif  4472  csbif  4531  disjors  5072  invdisjrab  5076  disjxiun  5086  disjxun  5087  sbcbr123  5143  eusvnf  5328  reusv2lem4  5337  reusv2  5339  moop2  5440  iunopeqop  5459  pofun  5540  opeliunxp  5681  opeliun2xp  5682  elrnmpt1  5897  resmptf  5985  csbima12  6025  csbcog  6240  fvmpt2f  6925  fvmpts  6927  fvmptdf  6930  fvmpt2i  6934  fvmptex  6938  fmptco  7057  fmptcof  7058  fmptcos  7059  elabrex  7171  elabrexg  7172  fliftfuns  7243  riotaeqimp  7324  csbov123  7385  ovmpos  7489  fvmpopr2d  7503  ofmpteq  7628  csbopeq1a  7977  mpomptsx  7991  dmmpossx  7993  fmpox  7994  el2mpocsbcl  8010  offval22  8013  ovmptss  8018  fmpoco  8020  mpoxeldm  8136  mpocurryd  8194  mpocurryvald  8195  fvmpocurryd  8196  eqerlem  8652  qliftfuns  8723  mptelixpg  8854  boxcutc  8860  xpf1o  9047  iunfi  9222  wdom2d  9461  ixpiunwdom  9471  hsmexlem2  10310  ac6c4  10364  iundom2g  10423  seqof2  13959  rlimcld2  15477  sumeq2ii  15592  summolem3  15613  summolem2a  15614  zsum  15617  fsum  15619  sumss2  15625  fsumcvg2  15626  fsumclf  15637  fsumzcl2  15638  fsumsplitf  15641  sumsnf  15642  fsumsplit1  15644  sumsns  15649  fsummsnunz  15653  fsumsplitsnun  15654  fsum2dlem  15669  fsumcnv  15672  fsumcom2  15673  fsumshftm  15680  fsum0diag2  15682  fsum00  15697  fsumabs  15700  fsumrlim  15710  fsumo1  15711  o1fsum  15712  fsumiun  15720  infcvgaux1i  15756  prodeq2ii  15810  prodmolem3  15832  prodmolem2a  15833  zprod  15836  fprod  15840  fprodntriv  15841  prodss  15846  fprodser  15848  fprodcllemf  15857  prodsn  15861  prodsnf  15863  fprodm1s  15869  fprodp1s  15870  prodsns  15871  fprodabs  15873  fprodn0  15878  fprod2dlem  15879  fprodcnv  15882  fprodcom2  15883  fproddivf  15886  fprodsplitf  15887  fprodsplit1f  15889  fprodle  15895  fprodmodd  15896  fprodefsum  15994  sumeven  16290  sumodd  16291  pcmpt  16796  pcmptdvds  16798  natpropd  17878  fucpropd  17879  gsummpt1n0  19870  gsumcom2  19880  gsummptnn0fz  19891  dprd2d2  19951  psrass1lem  21862  mpfrcl  22013  coe1fzgsumdlem  22211  gsumply1eq  22217  evl1gsumdlem  22264  mdetralt2  22517  mdetunilem2  22521  madugsum  22551  fiuncmp  23312  ptcld  23521  ptcldmpt  23522  ptclsg  23523  elmptrab  23735  prdsdsf  24275  prdsxmet  24277  fsumcn  24781  fsum2cn  24782  ovolfiniun  25422  ovoliunlem3  25425  ovoliun  25426  ovoliun2  25427  ovoliunnul  25428  finiunmbl  25465  volfiniun  25468  iundisj  25469  iundisj2  25470  iunmbl  25474  iunmbl2  25478  itgss3  25736  itgfsum  25748  itgabs  25756  limciun  25815  dvmptfsum  25899  dvfsumle  25946  dvfsumleOLD  25947  dvfsumabs  25949  dvfsumlem1  25952  dvfsumlem2  25953  dvfsumlem2OLD  25954  dvfsumlem3  25955  dvfsumlem4  25956  dvfsumrlim  25958  dvfsumrlim2  25959  dvfsum2  25961  itgsubstlem  25975  itgsubst  25976  rlimcnp2  26896  fsumdvdscom  27115  fsumdvdsmul  27125  fsumdvdsmulOLD  27127  fsumvma  27144  dchrisumlema  27419  dchrisumlem2  27421  dchrisumlem3  27422  ifeqeqx  32512  iunxpssiun1  32538  disjorsf  32550  disjabrex  32552  disjabrexf  32553  iundisjf  32559  iundisj2f  32560  disjunsn  32564  suppss2f  32610  2ndresdju  32621  fmptdF  32628  fmptcof2  32629  acunirnmpt2f  32633  aciunf1lem  32634  funcnv4mpt  32641  f1od2  32692  iundisjfi  32768  iundisj2fi  32769  fsumiunle  32802  gsummpt2co  33018  gsumpart  33027  gsumvsca1  33185  gsumvsca2  33186  rmfsupp2  33195  esumpfinvalf  34079  esum2dlem  34095  esumiun  34097  fiunelros  34177  measiun  34221  voliune  34232  volfiniune  34233  sbcaltop  35994  weiunpo  36478  weiunso  36479  weiunfr  36480  weiunse  36481  bj-sbeqALT  36913  rdgssun  37391  finxpreclem2  37403  phpreu  37623  finixpnum  37624  ptrest  37638  poimirlem23  37662  poimirlem24  37663  poimirlem25  37664  poimirlem26  37665  poimirlem27  37666  poimirlem28  37667  mbfposadd  37686  itgabsnc  37708  ftc1cnnclem  37710  ftc2nc  37721  fsumshftd  38970  riotasv2s  38976  cdleme31sn  40398  cdleme31sn1  40399  cdleme31se2  40401  cdleme32fva  40455  cdleme42b  40496  hlhilset  41952  evl1gprodd  42129  idomnnzgmulnz  42145  deg1gprod  42152  fmpocos  42246  mzpsubst  42760  rabdiophlem2  42814  elnn0rabdioph  42815  dvdsrabdioph  42822  fphpd  42828  monotuz  42953  oddcomabszz  42956  aomclem6  43071  flcidc  43182  fsumcnf  45037  sumsnd  45042  fiiuncl  45081  eliin2f  45120  disjf1  45199  disjrnmpt2  45204  disjinfi  45208  fmptf  45255  fmptff  45285  iuneqfzuzlem  45352  supxrleubrnmptf  45468  fsummulc1f  45590  fsumnncl  45591  fsumf1of  45593  fsumiunss  45594  fsumreclf  45595  fsumlessf  45596  fsumsermpt  45598  fprodexp  45613  fprodabs2  45614  mccllem  45616  fprodcnlem  45618  fprodcn  45619  climsubmpt  45677  climeldmeqmpt  45685  climfveqmpt  45688  climfveqmpt3  45699  climeldmeqmpt3  45706  climinf2mpt  45731  climinfmpt  45732  limsupequzmptf  45748  fprodcncf  45917  dvmptmulf  45954  dvnmptdivc  45955  dvmptfprod  45962  iblsplitf  45987  fourierdlem86  46209  fourierdlem112  46235  sge0f1o  46399  sge0lempt  46427  sge0iunmptlemfi  46430  sge0iunmptlemre  46432  sge0iunmpt  46435  sge0ltfirpmpt2  46443  sge0isummpt2  46449  sge0xaddlem2  46451  sge0xadd  46452  meadjiun  46483  hoimbl2  46682  vonhoire  46689  vonn0ioo2  46707  vonn0icc2  46709  csbafv12g  47147  csbaovg  47190  csbafv212g  47229  fsummsndifre  47382  fsumsplitsndif  47383  fsummmodsndifre  47384  fsummmodsnunz  47385  dmmpossx2  48347