Theorem csbeq1a 3403

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

Syntax hints:   -> wi 4   = wceq 1370   [_csb 3394

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-sbc 3293  df-csb 3395

This theorem is referenced by:  csbhypf  3413  csbiebt  3414  cbvralcsf  3426  cbvreucsf  3428  cbvrabcsf  3429  sbcnestgf  3798  csbun  3816  csbungOLD  3817  csbin  3819  csbingOLD  3820  csbif  3946  csbifgOLD  3947  csbopg  4184  disjors  4385  disjxiun  4396  disjxun  4397  sbcbr123  4450  sbcbrgOLD  4451  eusvnf  4594  reusv2lem4  4603  reusv2  4605  moop2  4693  pofun  4764  opeliunxp  4997  elrnmpt1  5195  csbima12  5293  csbima12gOLD  5294  fvmpts  5884  fvmpt2i  5888  fvmptex  5892  fmptco  5984  fmptcof  5985  fmptcos  5986  elabrex  6068  fliftfuns  6115  csbov123  6230  csbovgOLD  6232  ovmpt2s  6323  ofmpteq  6447  csbopeq1a  6736  mpt2mptsx  6746  dmmpt2ssx  6748  fmpt2x  6749  offval22  6761  ovmptss  6763  fmpt2co  6765  mpt2curryd  6897  mpt2curryvald  6898  fvmpt2curryd  6899  eqerlem  7242  qliftfuns  7296  mptelixpg  7409  boxcutc  7415  xpf1o  7582  iunfi  7709  wdom2d  7905  ixpiunwdom  7916  hsmexlem2  8706  ac6num  8758  ac6c4  8760  iundom2g  8814  seqof2  11980  rlimcld2  13173  sumeq2w  13286  sumeq2ii  13287  summolem3  13308  summolem2a  13309  zsum  13312  fsum  13314  sumss2  13320  fsumcvg2  13321  sumsn  13334  sumsns  13336  fsum2dlem  13354  fsumcnv  13357  fsumcom2  13358  fsumshftm  13365  fsum0diag2  13367  fsum00  13378  fsumabs  13381  fsumrlim  13391  fsumo1  13392  o1fsum  13393  fsumiun  13401  infcvgaux1i  13436  pcmpt  14071  pcmptdvds  14073  natpropd  15004  fucpropd  15005  gsummpt1n0  16577  gsumcom2  16588  dprd2d2  16664  psrass1lem  17569  mpfrcl  17727  evl1gsumdlem  17914  mdetralt2  18546  mdetunilem2  18550  madugsum  18580  fiuncmp  19138  ptcld  19317  ptcldmpt  19318  ptclsg  19319  elmptrab  19531  prdsdsf  20073  prdsxmet  20075  fsumcn  20577  fsum2cn  20578  ovolfiniun  21115  ovoliunlem3  21118  ovoliun  21119  ovoliun2  21120  ovoliunnul  21121  finiunmbl  21157  volfiniun  21160  iundisj  21161  iundisj2  21162  iunmbl  21166  iunmbl2  21170  itgss3  21424  itgfsum  21436  itgabs  21444  limciun  21501  dvmptfsum  21579  dvfsumle  21625  dvfsumabs  21627  dvfsumlem1  21630  dvfsumlem2  21631  dvfsumlem3  21632  dvfsumlem4  21633  dvfsumrlim  21635  dvfsumrlim2  21636  dvfsum2  21638  itgsubstlem  21652  itgsubst  21653  rlimcnp2  22492  fsumdvdscom  22657  fsumdvdsmul  22667  fsumvma  22684  dchrisumlema  22869  dchrisumlem2  22871  dchrisumlem3  22872  ifeqeqx  26053  disjorsf  26074  disjabrex  26076  disjabrexf  26077  iundisjf  26081  iundisj2f  26082  disjunsn  26086  suppss2f  26104  fmptdF  26122  resmptf  26124  fvmpt2f  26125  fmptcof2  26129  funcnv4mpt  26139  iundisjfi  26224  iundisj2fi  26225  gsummpt2co  26393  gsumvsca1  26395  gsumvsca2  26396  esumpfinvalf  26669  measiun  26776  voliune  26788  volfiniune  26789  prodeq2w  27568  prodeq2ii  27569  prodmolem3  27589  prodmolem2a  27590  zprod  27593  fprod  27597  fprodntriv  27598  prodss  27603  fprodser  27605  prodsn  27616  fprodm1s  27623  fprodp1s  27624  prodsns  27625  fprodabs  27627  fprodefsum  27628  fprodn0  27633  fprod2dlem  27634  fprodcnv  27637  fprodcom2  27638  sbcaltop  28155  finixpnum  28561  ptrest  28572  mbfposadd  28586  itgabsnc  28608  ftc1cnnclem  28612  ftc2nc  28623  mzpsubst  29232  rabdiophlem2  29287  elnn0rabdioph  29288  dvdsrabdioph  29295  fphpd  29302  monotuz  29429  oddcomabszz  29432  aomclem6  29559  flcidc  29678  fsumcnf  29890  sumsnd  29895  csbafv12g  30190  csbaovg  30233  fsumz  30383  fsummsndifre  30384  fsumsplitsndif  30385  fsummmodsndifre  30386  fsummsnunz  30388  fsumsplitsnun  30389  fsummmodsnunre  30390  opeliun2xp  30867  dmmpt2ssx2  30874  gsummptnn0fz  30957  coe1fzgsumdlem  30989  gsumply1eq  31005  bj-sbeqALT  32719  fsumshftd  32925  fsumshftdOLD  32926  riotasv2s  32932  cdleme31sn  34347  cdleme31sn1  34348  cdleme31se2  34350  cdleme32fva  34404  cdleme42b  34445  hlhilset  35905