Theorem csbeq1a 3404

Description: Equality theorem for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)

Assertion

Ref	Expression
csbeq1a	|- ( x = A -> B = [_ A / x ]_ B )

Proof of Theorem csbeq1a

Step	Hyp	Ref	Expression
1		csbid 3403	. 2 |- [_ x / x ]_ B = B
2		csbeq1 3398	. 2 |- ( x = A -> [_ x / x ]_ B = [_ A / x ]_ B )
3	1, 2	syl5eqr 2477	1 |- ( x = A -> B = [_ A / x ]_ B )

Syntax hints:   -> wi 4   = wceq 1437   [_csb 3395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-sbc 3300  df-csb 3396

This theorem is referenced by:  csbhypf  3414  csbiebt  3415  cbvralcsf  3427  cbvreucsf  3429  cbvrabcsf  3430  sbcnestgf  3814  csbun  3828  csbin  3829  csbif  3961  csbopg  4205  disjors  4409  invdisjrab  4413  disjxiun  4420  disjxun  4421  sbcbr123  4475  eusvnf  4619  reusv2lem4  4628  reusv2  4630  moop2  4715  pofun  4790  opeliunxp  4905  elrnmpt1  5102  csbima12  5204  csbima12gOLD  5205  fvmpt2f  5966  fvmpts  5968  fvmpt2i  5973  fvmptex  5977  fmptco  6072  fmptcof  6073  fmptcos  6074  elabrex  6164  fliftfuns  6223  csbov123  6340  ovmpt2s  6435  ofmpteq  6565  csbopeq1a  6861  mpt2mptsx  6871  dmmpt2ssx  6873  fmpt2x  6874  offval22  6887  ovmptss  6889  fmpt2co  6891  mpt2xeldm  6969  mpt2curryd  7028  mpt2curryvald  7029  fvmpt2curryd  7030  eqerlem  7407  qliftfuns  7462  mptelixpg  7571  boxcutc  7577  xpf1o  7744  iunfi  7872  wdom2d  8105  ixpiunwdom  8116  hsmexlem2  8865  ac6num  8917  ac6c4  8919  iundom2g  8973  seqof2  12278  rlimcld2  13642  sumeq2ii  13759  summolem3  13780  summolem2a  13781  zsum  13784  fsum  13786  sumss2  13792  fsumcvg2  13793  fsumzcl2  13804  sumsn  13807  sumsns  13811  fsummsnunz  13815  fsumsplitsnun  13816  fsum2dlem  13831  fsumcnv  13834  fsumcom2  13835  fsumshftm  13842  fsum0diag2  13844  fsum00  13858  fsumabs  13861  fsumrlim  13871  fsumo1  13872  o1fsum  13873  fsumiun  13881  infcvgaux1i  13915  prodeq2ii  13967  prodmolem3  13987  prodmolem2a  13988  zprod  13991  fprod  13995  fprodntriv  13996  prodss  14001  fprodser  14003  fprodcllemf  14012  prodsn  14016  prodsnf  14018  fprodm1s  14024  fprodp1s  14025  prodsns  14026  fprodabs  14028  fprodn0  14033  fprod2dlem  14034  fprodcnv  14037  fprodcom2  14038  fproddivf  14041  fprodsplitf  14042  fprodsplit1f  14044  fprodle  14050  fprodefsum  14149  pcmpt  14837  pcmptdvds  14839  natpropd  15881  fucpropd  15882  gsummpt1n0  17597  gsumcom2  17607  gsummptnn0fz  17615  dprd2d2  17677  psrass1lem  18601  mpfrcl  18741  coe1fzgsumdlem  18895  gsumply1eq  18899  evl1gsumdlem  18944  mdetralt2  19633  mdetunilem2  19637  madugsum  19667  fiuncmp  20418  ptcld  20627  ptcldmpt  20628  ptclsg  20629  elmptrab  20841  prdsdsf  21381  prdsxmet  21383  fsumcn  21901  fsum2cn  21902  ovolfiniun  22453  ovoliunlem3  22456  ovoliun  22457  ovoliun2  22458  ovoliunnul  22459  finiunmbl  22496  volfiniun  22499  iundisj  22500  iundisj2  22501  iunmbl  22505  iunmbl2  22509  itgss3  22771  itgfsum  22783  itgabs  22791  limciun  22848  dvmptfsum  22926  dvfsumle  22972  dvfsumabs  22974  dvfsumlem1  22977  dvfsumlem2  22978  dvfsumlem3  22979  dvfsumlem4  22980  dvfsumrlim  22982  dvfsumrlim2  22983  dvfsum2  22985  itgsubstlem  22999  itgsubst  23000  rlimcnp2  23891  fsumdvdscom  24113  fsumdvdsmul  24123  fsumvma  24140  dchrisumlema  24325  dchrisumlem2  24327  dchrisumlem3  24328  ifeqeqx  28161  disjorsf  28193  disjabrex  28195  disjabrexf  28196  iundisjf  28202  iundisj2f  28203  disjunsn  28207  suppss2fOLD  28240  suppss2f  28241  fmptdF  28258  resmptf  28260  fmptcof2  28262  acunirnmpt2f  28266  aciunf1lem  28267  funcnv4mpt  28276  iundisjfi  28379  iundisj2fi  28380  gsummpt2co  28551  gsumvsca1  28554  gsumvsca2  28555  esumpfinvalf  28906  esum2dlem  28922  esumiun  28924  fiunelros  29005  measiun  29049  voliune  29061  volfiniune  29062  sbcaltop  30754  bj-sbeqALT  31472  csbdif  31691  finxpreclem2  31747  phpreu  31894  finixpnum  31895  ptrest  31904  poimirlem23  31928  poimirlem24  31929  poimirlem25  31930  poimirlem26  31931  poimirlem27  31932  poimirlem28  31933  mbfposadd  31953  itgabsnc  31976  ftc1cnnclem  31980  ftc2nc  31991  fsumshftd  32493  fsumshftdOLD  32494  riotasv2s  32500  cdleme31sn  33917  cdleme31sn1  33918  cdleme31se2  33920  cdleme32fva  33974  cdleme42b  34015  hlhilset  35475  mzpsubst  35560  rabdiophlem2  35615  elnn0rabdioph  35616  dvdsrabdioph  35623  fphpd  35629  monotuz  35760  oddcomabszz  35763  aomclem6  35888  flcidc  36011  csbcog  36212  csbingOLD  37189  fsumcnf  37316  sumsnd  37321  elabrexg  37344  fiiuncl  37380  disjf1  37419  disjrnmpt2  37425  disjinfi  37430  iuneqfzuzlem  37512  fsumclf  37587  fsumsplitf  37588  fsummulc1f  37589  sumsnf  37590  fsumnncl  37592  fsumsplit1  37593  fsumf1of  37595  fsumiunss  37596  fsumreclf  37597  fsumlessf  37598  fprodexp  37615  fprodabs2  37616  mccllem  37618  fprodcncf  37720  dvmptmulf  37753  dvnmptdivc  37754  dvmptfprod  37761  iblsplitf  37788  fourierdlem86  37997  fourierdlem112  38023  sge0f1o  38133  sge0lempt  38161  sge0iunmptlemfi  38164  sge0iunmptlemre  38166  sge0iunmpt  38169  sge0ltfirpmpt2  38177  sge0isummpt2  38183  sge0xaddlem2  38185  sge0xadd  38186  meadjiun  38213  csbafv12g  38510  csbaovg  38553  iunopeqop  38871  fsummsndifre  38923  fsumsplitsndif  38924  fsummmodsndifre  38925  fsummmodsnunz  38926  opeliun2xp  39765  dmmpt2ssx2  39769