Theorem csbeq1a 3439

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 3438	. 2 |- [_ x / x ]_ B = B
2		csbeq1 3433	. 2 |- ( x = A -> [_ x / x ]_ B = [_ A / x ]_ B )
3	1, 2	syl5eqr 2512	1 |- ( x = A -> B = [_ A / x ]_ B )

Syntax hints:   -> wi 4   = wceq 1395   [_csb 3430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-sbc 3328  df-csb 3431

This theorem is referenced by:  csbhypf  3449  csbiebt  3450  cbvralcsf  3462  cbvreucsf  3464  cbvrabcsf  3465  sbcnestgf  3846  csbun  3862  csbin  3863  csbingOLD  3864  csbif  3994  csbifgOLD  3995  csbopg  4237  disjors  4442  invdisjrab  4446  disjxiun  4453  disjxun  4454  sbcbr123  4507  sbcbrgOLD  4508  eusvnf  4651  reusv2lem4  4660  reusv2  4662  moop2  4751  pofun  4825  opeliunxp  5060  elrnmpt1  5261  csbima12  5364  csbima12gOLD  5365  fvmpts  5958  fvmpt2i  5963  fvmptex  5967  fmptco  6065  fmptcof  6066  fmptcos  6067  elabrex  6156  fliftfuns  6213  csbov123  6330  ovmpt2s  6425  ofmpteq  6557  csbopeq1a  6852  mpt2mptsx  6862  dmmpt2ssx  6864  fmpt2x  6865  offval22  6878  ovmptss  6880  fmpt2co  6882  mpt2curryd  7016  mpt2curryvald  7017  fvmpt2curryd  7018  eqerlem  7361  qliftfuns  7416  mptelixpg  7525  boxcutc  7531  xpf1o  7698  iunfi  7826  wdom2d  8024  ixpiunwdom  8035  hsmexlem2  8824  ac6num  8876  ac6c4  8878  iundom2g  8932  seqof2  12167  rlimcld2  13412  sumeq2ii  13526  summolem3  13547  summolem2a  13548  zsum  13551  fsum  13553  sumss2  13559  fsumcvg2  13560  fsumzcl2  13571  sumsn  13574  sumsns  13576  fsummsnunz  13580  fsumsplitsnun  13581  fsum2dlem  13596  fsumcnv  13599  fsumcom2  13600  fsumshftm  13607  fsum0diag2  13609  fsum00  13623  fsumabs  13626  fsumrlim  13636  fsumo1  13637  o1fsum  13638  fsumiun  13646  infcvgaux1i  13679  prodeq2ii  13731  prodmolem3  13751  prodmolem2a  13752  zprod  13755  fprod  13759  fprodntriv  13760  prodss  13765  fprodser  13767  prodsn  13778  fprodm1s  13785  fprodp1s  13786  prodsns  13787  fprodabs  13789  fprodn0  13794  fprod2dlem  13795  fprodcnv  13798  fprodcom2  13799  fprodefsum  13841  pcmpt  14422  pcmptdvds  14424  natpropd  15391  fucpropd  15392  gsummpt1n0  17118  gsumcom2  17129  gsummptnn0fz  17140  dprd2d2  17219  psrass1lem  18155  mpfrcl  18313  coe1fzgsumdlem  18469  gsumply1eq  18473  evl1gsumdlem  18518  mdetralt2  19237  mdetunilem2  19241  madugsum  19271  fiuncmp  20030  ptcld  20239  ptcldmpt  20240  ptclsg  20241  elmptrab  20453  prdsdsf  20995  prdsxmet  20997  fsumcn  21499  fsum2cn  21500  ovolfiniun  22037  ovoliunlem3  22040  ovoliun  22041  ovoliun2  22042  ovoliunnul  22043  finiunmbl  22079  volfiniun  22082  iundisj  22083  iundisj2  22084  iunmbl  22088  iunmbl2  22092  itgss3  22346  itgfsum  22358  itgabs  22366  limciun  22423  dvmptfsum  22501  dvfsumle  22547  dvfsumabs  22549  dvfsumlem1  22552  dvfsumlem2  22553  dvfsumlem3  22554  dvfsumlem4  22555  dvfsumrlim  22557  dvfsumrlim2  22558  dvfsum2  22560  itgsubstlem  22574  itgsubst  22575  rlimcnp2  23421  fsumdvdscom  23586  fsumdvdsmul  23596  fsumvma  23613  dchrisumlema  23798  dchrisumlem2  23800  dchrisumlem3  23801  ifeqeqx  27552  disjorsf  27578  disjabrex  27580  disjabrexf  27581  iundisjf  27585  iundisj2f  27586  disjunsn  27590  suppss2f  27620  fmptdF  27638  resmptf  27640  fvmpt2f  27641  fmptcof2  27645  acunirnmpt2f  27649  aciunf1lem  27650  funcnv4mpt  27660  iundisjfi  27753  iundisj2fi  27754  gsummpt2co  27923  gsumvsca1  27926  gsumvsca2  27927  esumpfinvalf  28238  esum2dlem  28252  esumiun  28254  measiun  28350  voliune  28362  volfiniune  28363  sbcaltop  29793  finixpnum  30200  ptrest  30210  mbfposadd  30224  itgabsnc  30246  ftc1cnnclem  30250  ftc2nc  30261  mzpsubst  30843  rabdiophlem2  30897  elnn0rabdioph  30898  dvdsrabdioph  30905  fphpd  30912  monotuz  31039  oddcomabszz  31042  aomclem6  31167  flcidc  31285  fsumcnf  31557  sumsnd  31562  elabrexg  31591  fsumclf  31728  fsumsplitf  31729  fsummulc1f  31730  sumsnf  31731  fsumnncl  31733  fsumsplit1  31734  prodsnf  31748  fproddivf  31749  fprodsplitf  31750  fprodcllemf  31752  fprodsplit1f  31754  fprodexp  31761  fprodabs2  31763  fprodle  31765  mccllem  31766  fprodcncf  31865  dvmptmulf  31895  dvnmptdivc  31896  dvmptfprod  31903  iblsplitf  31930  fourierdlem86  32136  fourierdlem112  32162  csbafv12g  32383  csbaovg  32426  fsummsndifre  32565  fsumsplitsndif  32566  fsummmodsndifre  32567  fsummmodsnunz  32568  opeliun2xp  33024  dmmpt2ssx2  33028  bj-sbeqALT  34568  fsumshftd  34783  fsumshftdOLD  34784  riotasv2s  34790  cdleme31sn  36207  cdleme31sn1  36208  cdleme31se2  36210  cdleme32fva  36264  cdleme42b  36305  hlhilset  37765