Theorem csbeq1a 3851

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

Syntax hints:   → wi 4   = wceq 1539  ⦋csb 3837

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-12 2169  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-sbc 3722  df-csb 3838

This theorem is referenced by:  csbhypf  3866  csbiebt  3867  cbvrabcsfw  3881  cbvralcsf  3882  cbvreucsf  3884  cbvrabcsf  3885  rspc2vd  3888  sbcnestgfw  4358  sbcnestgf  4363  csbun  4378  csbin  4379  csbdif  4464  csbif  4522  disjors  5062  invdisjrabw  5066  invdisjrab  5067  disjxiun  5078  disjxun  5079  sbcbr123  5135  eusvnf  5324  reusv2lem4  5333  reusv2  5335  moop2  5429  iunopeqop  5448  pofun  5532  opeliunxp  5665  elrnmpt1  5879  resmptf  5959  csbima12  5997  csbcog  6215  fvmpt2f  6908  fvmpts  6910  fvmptdf  6913  fvmpt2i  6917  fvmptex  6921  fmptco  7033  fmptcof  7034  fmptcos  7035  elabrex  7148  fliftfuns  7217  riotaeqimp  7291  csbov123  7349  ovmpos  7453  fvmpopr2d  7466  ofmpteq  7587  csbopeq1a  7923  mpomptsx  7936  dmmpossx  7938  fmpox  7939  el2mpocsbcl  7957  offval22  7960  ovmptss  7965  fmpoco  7967  mpoxeldm  8058  mpocurryd  8116  mpocurryvald  8117  fvmpocurryd  8118  eqerlem  8563  qliftfuns  8624  mptelixpg  8754  boxcutc  8760  xpf1o  8964  iunfi  9151  wdom2d  9383  ixpiunwdom  9393  hsmexlem2  10229  ac6c4  10283  iundom2g  10342  seqof2  13827  rlimcld2  15332  sumeq2ii  15450  summolem3  15471  summolem2a  15472  zsum  15475  fsum  15477  sumss2  15483  fsumcvg2  15484  fsumclf  15495  fsumzcl2  15496  fsumsplitf  15499  sumsnf  15500  fsumsplit1  15502  sumsns  15507  fsummsnunz  15511  fsumsplitsnun  15512  fsum2dlem  15527  fsumcnv  15530  fsumcom2  15531  fsumshftm  15538  fsum0diag2  15540  fsum00  15555  fsumabs  15558  fsumrlim  15568  fsumo1  15569  o1fsum  15570  fsumiun  15578  infcvgaux1i  15614  prodeq2ii  15668  prodmolem3  15688  prodmolem2a  15689  zprod  15692  fprod  15696  fprodntriv  15697  prodss  15702  fprodser  15704  fprodcllemf  15713  prodsn  15717  prodsnf  15719  fprodm1s  15725  fprodp1s  15726  prodsns  15727  fprodabs  15729  fprodn0  15734  fprod2dlem  15735  fprodcnv  15738  fprodcom2  15739  fproddivf  15742  fprodsplitf  15743  fprodsplit1f  15745  fprodle  15751  fprodmodd  15752  fprodefsum  15849  sumeven  16141  sumodd  16142  pcmpt  16638  pcmptdvds  16640  natpropd  17739  fucpropd  17740  gsummpt1n0  19611  gsumcom2  19621  gsummptnn0fz  19632  dprd2d2  19692  psrass1lemOLD  21188  psrass1lem  21191  mpfrcl  21340  coe1fzgsumdlem  21517  gsumply1eq  21521  evl1gsumdlem  21567  mdetralt2  21803  mdetunilem2  21807  madugsum  21837  fiuncmp  22600  ptcld  22809  ptcldmpt  22810  ptclsg  22811  elmptrab  23023  prdsdsf  23565  prdsxmet  23567  fsumcn  24078  fsum2cn  24079  ovolfiniun  24710  ovoliunlem3  24713  ovoliun  24714  ovoliun2  24715  ovoliunnul  24716  finiunmbl  24753  volfiniun  24756  iundisj  24757  iundisj2  24758  iunmbl  24762  iunmbl2  24766  itgss3  25024  itgfsum  25036  itgabs  25044  limciun  25103  dvmptfsum  25184  dvfsumle  25230  dvfsumabs  25232  dvfsumlem1  25235  dvfsumlem2  25236  dvfsumlem3  25237  dvfsumlem4  25238  dvfsumrlim  25240  dvfsumrlim2  25241  dvfsum2  25243  itgsubstlem  25257  itgsubst  25258  rlimcnp2  26161  fsumdvdscom  26379  fsumdvdsmul  26389  fsumvma  26406  dchrisumlema  26681  dchrisumlem2  26683  dchrisumlem3  26684  ifeqeqx  30930  disjorsf  30964  disjabrex  30966  disjabrexf  30967  iundisjf  30973  iundisj2f  30974  disjunsn  30978  suppss2f  31019  2ndresdju  31031  fmptdF  31038  fmptcof2  31039  acunirnmpt2f  31043  aciunf1lem  31044  funcnv4mpt  31051  f1od2  31101  iundisjfi  31162  iundisj2fi  31163  fsumiunle  31188  gsummpt2co  31353  gsumpart  31360  gsumvsca1  31524  gsumvsca2  31525  rmfsupp2  31537  esumpfinvalf  32089  esum2dlem  32105  esumiun  32107  fiunelros  32187  measiun  32231  voliune  32242  volfiniune  32243  sbcaltop  34328  bj-sbeqALT  35129  rdgssun  35593  finxpreclem2  35605  phpreu  35805  finixpnum  35806  ptrest  35820  poimirlem23  35844  poimirlem24  35845  poimirlem25  35846  poimirlem26  35847  poimirlem27  35848  poimirlem28  35849  mbfposadd  35868  itgabsnc  35890  ftc1cnnclem  35892  ftc2nc  35903  fsumshftd  37008  riotasv2s  37014  cdleme31sn  38436  cdleme31sn1  38437  cdleme31se2  38439  cdleme32fva  38493  cdleme42b  38534  hlhilset  39990  mzpsubst  40607  rabdiophlem2  40661  elnn0rabdioph  40662  dvdsrabdioph  40669  fphpd  40675  monotuz  40801  oddcomabszz  40804  aomclem6  40922  flcidc  41037  fsumcnf  42602  sumsnd  42607  elabrexg  42627  fiiuncl  42651  eliin2f  42692  disjf1  42764  disjrnmpt2  42770  disjinfi  42775  fmptf  42828  iuneqfzuzlem  42921  supxrleubrnmptf  43039  fsummulc1f  43161  fsumnncl  43162  fsumf1of  43164  fsumiunss  43165  fsumreclf  43166  fsumlessf  43167  fsumsermpt  43169  fprodexp  43184  fprodabs2  43185  mccllem  43187  fprodcnlem  43189  fprodcn  43190  climsubmpt  43250  climeldmeqmpt  43258  climfveqmpt  43261  climfveqmpt3  43272  climeldmeqmpt3  43279  climinf2mpt  43304  climinfmpt  43305  limsupequzmptf  43321  fprodcncf  43490  dvmptmulf  43527  dvnmptdivc  43528  dvmptfprod  43535  iblsplitf  43560  fourierdlem86  43782  fourierdlem112  43808  sge0f1o  43970  sge0lempt  43998  sge0iunmptlemfi  44001  sge0iunmptlemre  44003  sge0iunmpt  44006  sge0ltfirpmpt2  44014  sge0isummpt2  44020  sge0xaddlem2  44022  sge0xadd  44023  meadjiun  44054  hoimbl2  44253  vonhoire  44260  vonn0ioo2  44278  vonn0icc2  44280  csbafv12g  44687  csbaovg  44730  csbafv212g  44769  fsummsndifre  44882  fsumsplitsndif  44883  fsummmodsndifre  44884  fsummmodsnunz  44885  opeliun2xp  45726  dmmpossx2  45730