Theorem csbeq1a 3285

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

Syntax hints:   -> wi 4   = wceq 1362   [_csb 3276

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-sbc 3176  df-csb 3277

This theorem is referenced by:  csbhypf  3295  csbiebt  3296  cbvralcsf  3307  cbvreucsf  3309  cbvrabcsf  3310  sbcnestgf  3679  csbun  3697  csbungOLD  3698  csbin  3700  csbingOLD  3701  csbif  3827  csbifgOLD  3828  csbopg  4065  disjors  4266  disjxiun  4277  disjxun  4278  sbcbr123  4331  sbcbrgOLD  4332  eusvnf  4475  reusv2lem4  4484  reusv2  4486  moop2  4574  pofun  4644  opeliunxp  4877  elrnmpt1  5075  csbima12  5174  csbima12gOLD  5175  fvmpts  5764  fvmpt2i  5768  fvmptex  5772  fmptco  5863  fmptcof  5864  fmptcos  5865  elabrex  5947  fliftfuns  5994  csbov123  6111  csbovgOLD  6113  ovmpt2s  6203  ofmpteq  6327  csbopeq1a  6616  mpt2mptsx  6626  dmmpt2ssx  6628  fmpt2x  6629  offval22  6641  ovmptss  6643  fmpt2co  6645  eqerlem  7121  qliftfuns  7175  mptelixpg  7288  boxcutc  7294  xpf1o  7461  iunfi  7587  wdom2d  7783  ixpiunwdom  7794  hsmexlem2  8584  ac6num  8636  ac6c4  8638  iundom2g  8692  seqof2  11848  rlimcld2  13040  sumeq2w  13153  sumeq2ii  13154  summolem3  13175  summolem2a  13176  zsum  13179  fsum  13181  sumss2  13187  fsumcvg2  13188  sumsn  13201  sumsns  13203  fsum2dlem  13221  fsumcnv  13224  fsumcom2  13225  fsumshftm  13231  fsum0diag2  13233  fsum00  13244  fsumabs  13247  fsumrlim  13257  fsumo1  13258  o1fsum  13259  fsumiun  13267  infcvgaux1i  13302  pcmpt  13937  pcmptdvds  13939  natpropd  14869  fucpropd  14870  gsumcom2  16441  dprd2d2  16517  psrass1lem  17381  mdetralt2  18257  mdetunilem2  18261  madugsum  18291  fiuncmp  18849  ptcld  19028  ptcldmpt  19029  ptclsg  19030  elmptrab  19242  prdsdsf  19784  prdsxmet  19786  fsumcn  20288  fsum2cn  20289  ovolfiniun  20826  ovoliunlem3  20829  ovoliun  20830  ovoliun2  20831  ovoliunnul  20832  finiunmbl  20867  volfiniun  20870  iundisj  20871  iundisj2  20872  iunmbl  20876  iunmbl2  20880  itgss3  21134  itgfsum  21146  itgabs  21154  limciun  21211  dvmptfsum  21289  dvfsumle  21335  dvfsumabs  21337  dvfsumlem1  21340  dvfsumlem2  21341  dvfsumlem3  21342  dvfsumlem4  21343  dvfsumrlim  21345  dvfsumrlim2  21346  dvfsum2  21348  itgsubstlem  21362  itgsubst  21363  mpfrcl  21370  rlimcnp2  22245  fsumdvdscom  22410  fsumdvdsmul  22420  fsumvma  22437  dchrisumlema  22622  dchrisumlem2  22624  dchrisumlem3  22625  ifeqeqx  25726  disjorsf  25748  disjabrex  25750  disjabrexf  25751  iundisjf  25755  iundisj2f  25756  disjunsn  25760  suppss2f  25778  fmptdF  25796  resmptf  25798  fvmpt2f  25799  fmptcof2  25803  funcnv4mpt  25813  iundisjfi  25903  iundisj2fi  25904  gsummpt2co  26101  gsumvsca1  26104  gsumvsca2  26105  esumpfinvalf  26379  measiun  26486  voliune  26499  volfiniune  26500  prodeq2w  27272  prodeq2ii  27273  prodmolem3  27293  prodmolem2a  27294  zprod  27297  fprod  27301  fprodntriv  27302  prodss  27307  fprodser  27309  prodsn  27320  fprodm1s  27327  fprodp1s  27328  prodsns  27329  fprodabs  27331  fprodefsum  27332  fprodn0  27337  fprod2dlem  27338  fprodcnv  27341  fprodcom2  27342  sbcaltop  27859  finixpnum  28258  ptrest  28269  mbfposadd  28283  itgabsnc  28305  ftc1cnnclem  28309  ftc2nc  28320  mzpsubst  28930  rabdiophlem2  28985  elnn0rabdioph  28986  dvdsrabdioph  28993  fphpd  29000  monotuz  29127  oddcomabszz  29130  aomclem6  29257  flcidc  29376  fsumcnf  29588  sumsnd  29593  csbafv12g  29889  csbaovg  29932  fsumz  30082  fsummsndifre  30083  fsumsplitsndif  30084  fsummmodsndifre  30085  fsummsnunz  30087  fsumsplitsnun  30088  fsummmodsnunre  30089  opeliun2xp  30565  dmmpt2ssx2  30572  bj-sbeqALT  32017  riotasv2s  32203  cdleme31sn  33618  cdleme31sn1  33619  cdleme31se2  33621  cdleme32fva  33675  cdleme42b  33716  hlhilset  35176