Theorem csbeq1a 3292

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

Syntax hints:   -> wi 4   = wceq 1369   [_csb 3283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-sbc 3182  df-csb 3284

This theorem is referenced by:  csbhypf  3302  csbiebt  3303  cbvralcsf  3314  cbvreucsf  3316  cbvrabcsf  3317  sbcnestgf  3686  csbun  3704  csbungOLD  3705  csbin  3707  csbingOLD  3708  csbif  3834  csbifgOLD  3835  csbopg  4072  disjors  4273  disjxiun  4284  disjxun  4285  sbcbr123  4338  sbcbrgOLD  4339  eusvnf  4482  reusv2lem4  4491  reusv2  4493  moop2  4581  pofun  4652  opeliunxp  4885  elrnmpt1  5083  csbima12  5181  csbima12gOLD  5182  fvmpts  5771  fvmpt2i  5775  fvmptex  5779  fmptco  5871  fmptcof  5872  fmptcos  5873  elabrex  5955  fliftfuns  6002  csbov123  6117  csbovgOLD  6119  ovmpt2s  6209  ofmpteq  6333  csbopeq1a  6622  mpt2mptsx  6632  dmmpt2ssx  6634  fmpt2x  6635  offval22  6647  ovmptss  6649  fmpt2co  6651  eqerlem  7125  qliftfuns  7179  mptelixpg  7292  boxcutc  7298  xpf1o  7465  iunfi  7591  wdom2d  7787  ixpiunwdom  7798  hsmexlem2  8588  ac6num  8640  ac6c4  8642  iundom2g  8696  seqof2  11856  rlimcld2  13048  sumeq2w  13161  sumeq2ii  13162  summolem3  13183  summolem2a  13184  zsum  13187  fsum  13189  sumss2  13195  fsumcvg2  13196  sumsn  13209  sumsns  13211  fsum2dlem  13229  fsumcnv  13232  fsumcom2  13233  fsumshftm  13240  fsum0diag2  13242  fsum00  13253  fsumabs  13256  fsumrlim  13266  fsumo1  13267  o1fsum  13268  fsumiun  13276  infcvgaux1i  13311  pcmpt  13946  pcmptdvds  13948  natpropd  14878  fucpropd  14879  gsumcom2  16455  dprd2d2  16531  psrass1lem  17424  mpfrcl  17579  evl1gsumdlem  17765  mdetralt2  18390  mdetunilem2  18394  madugsum  18424  fiuncmp  18982  ptcld  19161  ptcldmpt  19162  ptclsg  19163  elmptrab  19375  prdsdsf  19917  prdsxmet  19919  fsumcn  20421  fsum2cn  20422  ovolfiniun  20959  ovoliunlem3  20962  ovoliun  20963  ovoliun2  20964  ovoliunnul  20965  finiunmbl  21000  volfiniun  21003  iundisj  21004  iundisj2  21005  iunmbl  21009  iunmbl2  21013  itgss3  21267  itgfsum  21279  itgabs  21287  limciun  21344  dvmptfsum  21422  dvfsumle  21468  dvfsumabs  21470  dvfsumlem1  21473  dvfsumlem2  21474  dvfsumlem3  21475  dvfsumlem4  21476  dvfsumrlim  21478  dvfsumrlim2  21479  dvfsum2  21481  itgsubstlem  21495  itgsubst  21496  rlimcnp2  22335  fsumdvdscom  22500  fsumdvdsmul  22510  fsumvma  22527  dchrisumlema  22712  dchrisumlem2  22714  dchrisumlem3  22715  ifeqeqx  25853  disjorsf  25875  disjabrex  25877  disjabrexf  25878  iundisjf  25882  iundisj2f  25883  disjunsn  25887  suppss2f  25905  fmptdF  25923  resmptf  25925  fvmpt2f  25926  fmptcof2  25930  funcnv4mpt  25940  iundisjfi  26031  iundisj2fi  26032  gsummpt2co  26200  gsumvsca1  26202  gsumvsca2  26203  esumpfinvalf  26477  measiun  26584  voliune  26597  volfiniune  26598  prodeq2w  27376  prodeq2ii  27377  prodmolem3  27397  prodmolem2a  27398  zprod  27401  fprod  27405  fprodntriv  27406  prodss  27411  fprodser  27413  prodsn  27424  fprodm1s  27431  fprodp1s  27432  prodsns  27433  fprodabs  27435  fprodefsum  27436  fprodn0  27441  fprod2dlem  27442  fprodcnv  27445  fprodcom2  27446  sbcaltop  27963  finixpnum  28367  ptrest  28378  mbfposadd  28392  itgabsnc  28414  ftc1cnnclem  28418  ftc2nc  28429  mzpsubst  29038  rabdiophlem2  29093  elnn0rabdioph  29094  dvdsrabdioph  29101  fphpd  29108  monotuz  29235  oddcomabszz  29238  aomclem6  29365  flcidc  29484  fsumcnf  29696  sumsnd  29701  csbafv12g  29996  csbaovg  30039  fsumz  30189  fsummsndifre  30190  fsumsplitsndif  30191  fsummmodsndifre  30192  fsummsnunz  30194  fsumsplitsnun  30195  fsummmodsnunre  30196  opeliun2xp  30672  dmmpt2ssx2  30679  bj-sbeqALT  32251  riotasv2s  32449  cdleme31sn  33864  cdleme31sn1  33865  cdleme31se2  33867  cdleme32fva  33921  cdleme42b  33962  hlhilset  35422