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 2811	1 ⊢ (𝑥 = 𝐴 → 𝐵 = ⦋𝐴 / 𝑥⦌𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1569  ⦋csb 3852

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-12 2212  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-sbc 3744  df-csb 3853

This theorem is used 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  5362  reusv2lem4  5371  reusv2  5373  moop2  5484  iunopeqop  5503  iunopeqopOLD  5504  pofun  5586  opeliunxp  5727  opeliun2xp  5728  elrnmpt1  5949  resmptf  6040  csbima12  6080  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  7395  csbov123  7456  ovmpos  7560  fvmpopr2d  7574  ofmpteq  7699  csbopeq1a  8045  mpomptsx  8059  dmmpossx  8061  fmpox  8062  el2mpocsbcl  8078  offval22  8081  ovmptss  8086  fmpoco  8088  mpoxeldm  8205  mpocurryd  8263  mpocurryvald  8264  fvmpocurryd  8265  eqerlem  8728  qliftfuns  8800  mptelixpg  8931  boxcutc  8937  xpf1o  9125  iunfi  9298  wdom2d  9540  ixpiunwdom  9550  hsmexlem2  10417  ac6c4  10471  iundom2g  10530  seqof2  14103  rlimcld2  15636  sumeq2ii  15751  summolem3  15772  summolem2a  15773  zsum  15776  fsum  15778  sumss2  15784  fsumcvg2  15785  fsumclf  15796  fsumzcl2  15797  fsumsplitf  15800  sumsnf  15801  fsumsplit1  15803  sumsns  15808  fsummsnunz  15812  fsumsplitsnun  15813  fsum2dlem  15828  fsumcnv  15831  fsumcom2  15832  fsumshftm  15839  fsum0diag2  15841  fsum00  15857  fsumabs  15860  fsumrlim  15870  fsumo1  15871  o1fsum  15872  fsumiun  15880  infcvgaux1i  15918  prodeq2ii  15972  prodmolem3  15994  prodmolem2a  15995  zprod  15998  fprod  16002  fprodntriv  16003  prodss  16008  fprodser  16010  fprodcllemf  16019  prodsn  16023  prodsnf  16025  fprodm1s  16031  fprodp1s  16032  prodsns  16033  fprodabs  16035  fprodn0  16040  fprod2dlem  16041  fprodcnv  16044  fprodcom2  16045  fproddivf  16048  fprodsplitf  16049  fprodsplit1f  16051  fprodle  16057  fprodmodd  16058  fprodefsum  16155  sumeven  16451  sumodd  16452  pcmpt  16958  pcmptdvds  16960  natpropd  18042  fucpropd  18043  gsummpt1n0  20041  gsumcom2  20051  gsummptnn0fz  20062  dprd2d2  20122  psrass1lem  22094  mpfrcl  22247  coe1fzgsumdlem  22474  gsumply1eq  22480  evl1gsumdlem  22527  mdetralt2  22777  mdetunilem2  22781  madugsum  22811  fiuncmp  23572  ptcld  23781  ptcldmpt  23782  ptclsg  23783  elmptrab  23995  prdsdsf  24535  prdsxmet  24537  fsumcn  25040  fsum2cn  25041  ovolfiniun  25671  ovoliunlem3  25674  ovoliun  25675  ovoliun2  25676  ovoliunnul  25677  finiunmbl  25714  volfiniun  25717  iundisj  25718  iundisj2  25719  iunmbl  25723  iunmbl2  25727  itgss3  25985  itgfsum  25997  itgabs  26005  limciun  26064  dvmptfsum  26145  dvfsumle  26191  dvfsumabs  26193  dvfsumlem1  26196  dvfsumlem2  26197  dvfsumlem3  26198  dvfsumlem4  26199  dvfsumrlim  26201  dvfsumrlim2  26202  dvfsum2  26204  itgsubstlem  26218  itgsubst  26219  rlimcnp2  27142  fsumdvdscom  27360  fsumdvdsmul  27370  fsumvma  27388  dchrisumlema  27663  dchrisumlem2  27665  dchrisumlem3  27666  ifeqeqx  32899  iunxpssiun1  32924  disjorsf  32936  disjabrex  32938  disjabrexf  32939  iundisjf  32945  iundisj2f  32946  disjunsn  32950  suppss2f  32994  2ndresdju  33005  fmptdF  33012  fmptcof2  33013  acunirnmpt2f  33017  aciunf1lem  33018  funcnv4mpt  33024  f1od2  33075  iundisjfi  33152  iundisj2fi  33153  fsumiunle  33184  gsummpt2co  33377  gsummptp1  33386  gsumpart  33392  gsumvsca1  33555  gsumvsca2  33556  rmfsupp2  33566  esumpfinvalf  34475  esum2dlem  34491  esumiun  34493  fiunelros  34573  measiun  34617  voliune  34628  volfiniune  34629  sbcaltop  36481  weiunpo  37004  weiunso  37005  weiunfr  37006  weiunse  37007  csbttc  37048  bj-sbeqALT  37563  rdgssun  38052  finxpreclem2  38064  phpreu  38283  finixpnum  38284  ptrest  38298  poimirlem23  38322  poimirlem24  38323  poimirlem25  38324  poimirlem26  38325  poimirlem27  38326  poimirlem28  38327  mbfposadd  38346  itgabsnc  38368  ftc1cnnclem  38370  ftc2nc  38381  fsumshftd  39754  riotasv2s  39760  cdleme31sn  41182  cdleme31sn1  41183  cdleme31se2  41185  cdleme32fva  41239  cdleme42b  41280  hlhilset  42736  evl1gprodd  42912  idomnnzgmulnz  42928  deg1gprod  42935  fmpocos  43032  mzpsubst  43507  rabdiophlem2  43557  elnn0rabdioph  43558  dvdsrabdioph  43565  fphpd  43571  monotuz  43696  oddcomabszz  43699  aomclem6  43814  flcidc  43925  fsumcnf  45769  sumsnd  45774  fiiuncl  45813  eliin2f  45850  disjf1  45929  disjrnmpt2  45934  disjinfi  45938  fmptf  45982  fmptff  46012  iuneqfzuzlem  46078  supxrleubrnmptf  46193  fsummulc1f  46315  fsumnncl  46316  fsumf1of  46318  fsumiunss  46319  fsumreclf  46320  fsumlessf  46321  fsumsermpt  46323  fprodexp  46338  fprodabs2  46339  mccllem  46341  fprodcnlem  46343  fprodcn  46344  climsubmpt  46402  climeldmeqmpt  46410  climfveqmpt  46413  climfveqmpt3  46424  climeldmeqmpt3  46431  climinf2mpt  46456  climinfmpt  46457  limsupequzmptf  46473  fprodcncf  46642  dvmptmulf  46679  dvnmptdivc  46680  dvmptfprod  46687  iblsplitf  46712  fourierdlem86  46934  fourierdlem112  46960  sge0f1o  47124  sge0lempt  47152  sge0iunmptlemfi  47155  sge0iunmptlemre  47157  sge0iunmpt  47160  sge0ltfirpmpt2  47168  sge0isummpt2  47174  sge0xaddlem2  47176  sge0xadd  47177  meadjiun  47208  hoimbl2  47407  vonhoire  47414  vonn0ioo2  47432  vonn0icc2  47434  csbafv12g  47902  csbaovg  47945  csbafv212g  47984  fsummsndifre  48145  fsumsplitsndif  48146  fsummmodsndifre  48147  fsummmodsnunz  48148  dmmpossx2  49145