Theorem csbeq1a 3906

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

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

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 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-sbc 3777  df-csb 3893

This theorem is referenced by:  csbhypf  3921  csbiebt  3922  cbvrabcsfw  3936  cbvralcsf  3937  cbvreucsf  3939  cbvrabcsf  3940  rspc2vd  3943  sbcnestgfw  4417  sbcnestgf  4422  csbun  4437  csbin  4438  csbdif  4526  csbif  4584  disjors  5128  invdisjrabw  5132  invdisjrab  5133  disjxiun  5144  disjxun  5145  sbcbr123  5201  eusvnf  5389  reusv2lem4  5398  reusv2  5400  moop2  5501  iunopeqop  5520  pofun  5605  opeliunxp  5742  elrnmpt1  5956  resmptf  6038  csbima12  6077  csbcog  6295  fvmpt2f  6998  fvmpts  7000  fvmptdf  7003  fvmpt2i  7007  fvmptex  7011  fmptco  7128  fmptcof  7129  fmptcos  7130  elabrex  7243  elabrexg  7244  fliftfuns  7313  riotaeqimp  7394  csbov123  7453  ovmpos  7558  fvmpopr2d  7571  ofmpteq  7694  csbopeq1a  8038  mpomptsx  8052  dmmpossx  8054  fmpox  8055  el2mpocsbcl  8073  offval22  8076  ovmptss  8081  fmpoco  8083  mpoxeldm  8198  mpocurryd  8256  mpocurryvald  8257  fvmpocurryd  8258  eqerlem  8739  qliftfuns  8800  mptelixpg  8931  boxcutc  8937  xpf1o  9141  iunfi  9342  wdom2d  9577  ixpiunwdom  9587  hsmexlem2  10424  ac6c4  10478  iundom2g  10537  seqof2  14030  rlimcld2  15526  sumeq2ii  15643  summolem3  15664  summolem2a  15665  zsum  15668  fsum  15670  sumss2  15676  fsumcvg2  15677  fsumclf  15688  fsumzcl2  15689  fsumsplitf  15692  sumsnf  15693  fsumsplit1  15695  sumsns  15700  fsummsnunz  15704  fsumsplitsnun  15705  fsum2dlem  15720  fsumcnv  15723  fsumcom2  15724  fsumshftm  15731  fsum0diag2  15733  fsum00  15748  fsumabs  15751  fsumrlim  15761  fsumo1  15762  o1fsum  15763  fsumiun  15771  infcvgaux1i  15807  prodeq2ii  15861  prodmolem3  15881  prodmolem2a  15882  zprod  15885  fprod  15889  fprodntriv  15890  prodss  15895  fprodser  15897  fprodcllemf  15906  prodsn  15910  prodsnf  15912  fprodm1s  15918  fprodp1s  15919  prodsns  15920  fprodabs  15922  fprodn0  15927  fprod2dlem  15928  fprodcnv  15931  fprodcom2  15932  fproddivf  15935  fprodsplitf  15936  fprodsplit1f  15938  fprodle  15944  fprodmodd  15945  fprodefsum  16042  sumeven  16334  sumodd  16335  pcmpt  16829  pcmptdvds  16831  natpropd  17933  fucpropd  17934  gsummpt1n0  19874  gsumcom2  19884  gsummptnn0fz  19895  dprd2d2  19955  psrass1lemOLD  21712  psrass1lem  21715  mpfrcl  21867  coe1fzgsumdlem  22045  gsumply1eq  22049  evl1gsumdlem  22095  mdetralt2  22331  mdetunilem2  22335  madugsum  22365  fiuncmp  23128  ptcld  23337  ptcldmpt  23338  ptclsg  23339  elmptrab  23551  prdsdsf  24093  prdsxmet  24095  fsumcn  24608  fsum2cn  24609  ovolfiniun  25250  ovoliunlem3  25253  ovoliun  25254  ovoliun2  25255  ovoliunnul  25256  finiunmbl  25293  volfiniun  25296  iundisj  25297  iundisj2  25298  iunmbl  25302  iunmbl2  25306  itgss3  25564  itgfsum  25576  itgabs  25584  limciun  25643  dvmptfsum  25727  dvfsumle  25773  dvfsumabs  25775  dvfsumlem1  25778  dvfsumlem2  25779  dvfsumlem3  25780  dvfsumlem4  25781  dvfsumrlim  25783  dvfsumrlim2  25784  dvfsum2  25786  itgsubstlem  25800  itgsubst  25801  rlimcnp2  26707  fsumdvdscom  26925  fsumdvdsmul  26935  fsumvma  26952  dchrisumlema  27227  dchrisumlem2  27229  dchrisumlem3  27230  ifeqeqx  32041  disjorsf  32078  disjabrex  32080  disjabrexf  32081  iundisjf  32087  iundisj2f  32088  disjunsn  32092  suppss2f  32130  2ndresdju  32141  fmptdF  32148  fmptcof2  32149  acunirnmpt2f  32153  aciunf1lem  32154  funcnv4mpt  32161  f1od2  32213  iundisjfi  32274  iundisj2fi  32275  fsumiunle  32302  gsummpt2co  32470  gsumpart  32477  gsumvsca1  32641  gsumvsca2  32642  rmfsupp2  32657  esumpfinvalf  33372  esum2dlem  33388  esumiun  33390  fiunelros  33470  measiun  33514  voliune  33525  volfiniune  33526  sbcaltop  35257  gg-dvfsumle  35468  gg-dvfsumlem2  35469  bj-sbeqALT  36083  rdgssun  36562  finxpreclem2  36574  phpreu  36775  finixpnum  36776  ptrest  36790  poimirlem23  36814  poimirlem24  36815  poimirlem25  36816  poimirlem26  36817  poimirlem27  36818  poimirlem28  36819  mbfposadd  36838  itgabsnc  36860  ftc1cnnclem  36862  ftc2nc  36873  fsumshftd  38125  riotasv2s  38131  cdleme31sn  39554  cdleme31sn1  39555  cdleme31se2  39557  cdleme32fva  39611  cdleme42b  39652  hlhilset  41108  fmpocos  41362  mzpsubst  41788  rabdiophlem2  41842  elnn0rabdioph  41843  dvdsrabdioph  41850  fphpd  41856  monotuz  41982  oddcomabszz  41985  aomclem6  42103  flcidc  42218  fsumcnf  44007  sumsnd  44012  fiiuncl  44053  eliin2f  44094  disjf1  44180  disjrnmpt2  44185  disjinfi  44189  fmptf  44240  fmptff  44272  iuneqfzuzlem  44342  supxrleubrnmptf  44459  fsummulc1f  44585  fsumnncl  44586  fsumf1of  44588  fsumiunss  44589  fsumreclf  44590  fsumlessf  44591  fsumsermpt  44593  fprodexp  44608  fprodabs2  44609  mccllem  44611  fprodcnlem  44613  fprodcn  44614  climsubmpt  44674  climeldmeqmpt  44682  climfveqmpt  44685  climfveqmpt3  44696  climeldmeqmpt3  44703  climinf2mpt  44728  climinfmpt  44729  limsupequzmptf  44745  fprodcncf  44914  dvmptmulf  44951  dvnmptdivc  44952  dvmptfprod  44959  iblsplitf  44984  fourierdlem86  45206  fourierdlem112  45232  sge0f1o  45396  sge0lempt  45424  sge0iunmptlemfi  45427  sge0iunmptlemre  45429  sge0iunmpt  45432  sge0ltfirpmpt2  45440  sge0isummpt2  45446  sge0xaddlem2  45448  sge0xadd  45449  meadjiun  45480  hoimbl2  45679  vonhoire  45686  vonn0ioo2  45704  vonn0icc2  45706  csbafv12g  46143  csbaovg  46186  csbafv212g  46225  fsummsndifre  46338  fsumsplitsndif  46339  fsummmodsndifre  46340  fsummmodsnunz  46341  opeliun2xp  47096  dmmpossx2  47100