Theorem csbeq1a 3219

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

Syntax hints:   -> wi 4   = wceq 1649   [_csb 3211

This theorem is referenced by:  csbhypf  3246  csbiebt  3247  sbcnestgf  3258  cbvralcsf  3271  cbvreucsf  3273  cbvrabcsf  3274  csbing  3508  csbifg  3727  disjors  4158  disjxiun  4169  disjxun  4170  sbcbrg  4221  moop2  4411  pofun  4479  eusvnf  4677  reusv2lem4  4686  reusv2  4688  opeliunxp  4888  elrnmpt1  5078  csbima12g  5172  fvmpts  5766  fvmpt2i  5770  fvmptex  5774  fmptco  5860  fmptcof  5861  fmptcos  5862  elabrex  5944  fliftfuns  5995  csbovg  6071  ovmpt2s  6156  csbopeq1a  6359  mpt2mptsx  6373  dmmpt2ssx  6375  fmpt2x  6376  ovmptss  6387  fmpt2co  6389  riotasv2s  6555  eqerlem  6896  qliftfuns  6950  mptelixpg  7058  boxcutc  7064  xpf1o  7228  iunfi  7353  wdom2d  7504  ixpiunwdom  7515  hsmexlem2  8263  ac6num  8315  ac6c4  8317  iundom2g  8371  seqof2  11336  rlimcld2  12327  sumeq2w  12441  sumeq2ii  12442  summolem3  12463  summolem2a  12464  zsum  12467  fsum  12469  sumss2  12475  fsumcvg2  12476  sumsn  12489  sumsns  12491  fsum2dlem  12509  fsumcnv  12512  fsumcom2  12513  fsumshftm  12519  fsum0diag2  12521  fsum00  12532  fsumabs  12535  fsumrlim  12545  fsumo1  12546  o1fsum  12547  fsumiun  12555  infcvgaux1i  12591  pcmpt  13216  pcmptdvds  13218  natpropd  14128  fucpropd  14129  gsumcom2  15504  dprd2d2  15557  psrass1lem  16397  fiuncmp  17421  ptcld  17598  ptcldmpt  17599  ptclsg  17600  elmptrab  17812  prdsdsf  18350  prdsxmet  18352  fsumcn  18853  fsum2cn  18854  ovolfiniun  19350  ovoliunlem3  19353  ovoliun  19354  ovoliun2  19355  ovoliunnul  19356  finiunmbl  19391  volfiniun  19394  iundisj  19395  iundisj2  19396  iunmbl  19400  iunmbl2  19404  itgss3  19659  itgfsum  19671  itgabs  19679  limciun  19734  dvmptfsum  19812  dvfsumle  19858  dvfsumabs  19860  dvfsumlem1  19863  dvfsumlem2  19864  dvfsumlem3  19865  dvfsumlem4  19866  dvfsumrlim  19868  dvfsumrlim2  19869  dvfsum2  19871  itgsubstlem  19885  itgsubst  19886  mpfrcl  19892  rlimcnp2  20758  fsumdvdscom  20923  fsumdvdsmul  20933  fsumvma  20950  dchrisumlema  21135  dchrisumlem2  21137  dchrisumlem3  21138  ifeqeqx  23954  disjorsf  23975  disjabrex  23977  disjabrexf  23978  iundisjf  23982  iundisj2f  23983  suppss2f  24002  fmptdF  24022  resmptf  24024  fvmpt2f  24025  fmptcof2  24029  funcnv4mpt  24038  iundisjfi  24105  iundisj2fi  24106  esumpfinvalf  24419  measiun  24525  voliune  24538  volfiniune  24539  sbcung  25077  sbcopg  25079  prodeq2w  25191  prodeq2ii  25192  prodmolem3  25212  prodmolem2a  25213  zprod  25216  fprod  25220  fprodntriv  25221  prodss  25226  fprodser  25228  prodsn  25239  fprodm1s  25246  fprodp1s  25247  prodsns  25248  fprodabs  25250  fprodefsum  25251  fprodn0  25256  fprod2dlem  25257  fprodcnv  25260  fprodcom2  25261  sbcaltop  25730  itgabsnc  26173  ofmpteq  26666  mzpsubst  26695  rabdiophlem2  26752  elnn0rabdioph  26753  dvdsrabdioph  26760  fphpd  26767  monotuz  26894  oddcomabszz  26897  aomclem6  27024  flcidc  27247  fsumcnf  27559  sumsnd  27564  csbafv12g  27868  csbaovg  27911  cdleme31sn  30862  cdleme31sn1  30863  cdleme31se2  30865  cdleme32fva  30919  cdleme42b  30960  hlhilset  32420

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-sbc 3122  df-csb 3212