Theorem csbeq1a 3410

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 3409	. 2 |- [_ x / x ]_ B = B
2		csbeq1 3404	. 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 1437   [_csb 3401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-sbc 3306  df-csb 3402

This theorem is referenced by:  csbhypf  3420  csbiebt  3421  cbvralcsf  3433  cbvreucsf  3435  cbvrabcsf  3436  sbcnestgf  3818  csbun  3832  csbin  3833  csbif  3965  csbopg  4208  disjors  4412  invdisjrab  4416  disjxiun  4423  disjxun  4424  sbcbr123  4477  eusvnf  4620  reusv2lem4  4629  reusv2  4631  moop2  4716  pofun  4791  opeliunxp  4906  elrnmpt1  5103  csbima12  5205  csbima12gOLD  5206  fvmpt2f  5965  fvmpts  5967  fvmpt2i  5972  fvmptex  5976  fmptco  6071  fmptcof  6072  fmptcos  6073  elabrex  6163  fliftfuns  6222  csbov123  6339  ovmpt2s  6434  ofmpteq  6564  csbopeq1a  6860  mpt2mptsx  6870  dmmpt2ssx  6872  fmpt2x  6873  offval22  6886  ovmptss  6888  fmpt2co  6890  mpt2curryd  7024  mpt2curryvald  7025  fvmpt2curryd  7026  eqerlem  7403  qliftfuns  7458  mptelixpg  7567  boxcutc  7573  xpf1o  7740  iunfi  7868  wdom2d  8095  ixpiunwdom  8106  hsmexlem2  8855  ac6num  8907  ac6c4  8909  iundom2g  8963  seqof2  12268  rlimcld2  13620  sumeq2ii  13737  summolem3  13758  summolem2a  13759  zsum  13762  fsum  13764  sumss2  13770  fsumcvg2  13771  fsumzcl2  13782  sumsn  13785  sumsns  13789  fsummsnunz  13793  fsumsplitsnun  13794  fsum2dlem  13809  fsumcnv  13812  fsumcom2  13813  fsumshftm  13820  fsum0diag2  13822  fsum00  13836  fsumabs  13839  fsumrlim  13849  fsumo1  13850  o1fsum  13851  fsumiun  13859  infcvgaux1i  13893  prodeq2ii  13945  prodmolem3  13965  prodmolem2a  13966  zprod  13969  fprod  13973  fprodntriv  13974  prodss  13979  fprodser  13981  fprodcllemf  13990  prodsn  13994  prodsnf  13996  fprodm1s  14002  fprodp1s  14003  prodsns  14004  fprodabs  14006  fprodn0  14011  fprod2dlem  14012  fprodcnv  14015  fprodcom2  14016  fproddivf  14019  fprodsplitf  14020  fprodsplit1f  14022  fprodle  14028  fprodefsum  14127  pcmpt  14800  pcmptdvds  14802  natpropd  15832  fucpropd  15833  gsummpt1n0  17532  gsumcom2  17542  gsummptnn0fz  17550  dprd2d2  17612  psrass1lem  18536  mpfrcl  18676  coe1fzgsumdlem  18830  gsumply1eq  18834  evl1gsumdlem  18879  mdetralt2  19565  mdetunilem2  19569  madugsum  19599  fiuncmp  20350  ptcld  20559  ptcldmpt  20560  ptclsg  20561  elmptrab  20773  prdsdsf  21313  prdsxmet  21315  fsumcn  21798  fsum2cn  21799  ovolfiniun  22332  ovoliunlem3  22335  ovoliun  22336  ovoliun2  22337  ovoliunnul  22338  finiunmbl  22374  volfiniun  22377  iundisj  22378  iundisj2  22379  iunmbl  22383  iunmbl2  22387  itgss3  22649  itgfsum  22661  itgabs  22669  limciun  22726  dvmptfsum  22804  dvfsumle  22850  dvfsumabs  22852  dvfsumlem1  22855  dvfsumlem2  22856  dvfsumlem3  22857  dvfsumlem4  22858  dvfsumrlim  22860  dvfsumrlim2  22861  dvfsum2  22863  itgsubstlem  22877  itgsubst  22878  rlimcnp2  23757  fsumdvdscom  23977  fsumdvdsmul  23987  fsumvma  24004  dchrisumlema  24189  dchrisumlem2  24191  dchrisumlem3  24192  ifeqeqx  27997  disjorsf  28029  disjabrex  28031  disjabrexf  28032  iundisjf  28038  iundisj2f  28039  disjunsn  28043  suppss2fOLD  28077  suppss2f  28078  fmptdF  28095  resmptf  28097  fmptcof2  28099  acunirnmpt2f  28103  aciunf1lem  28104  funcnv4mpt  28113  iundisjfi  28208  iundisj2fi  28209  gsummpt2co  28381  gsumvsca1  28384  gsumvsca2  28385  esumpfinvalf  28736  esum2dlem  28752  esumiun  28754  fiunelros  28835  measiun  28879  voliune  28891  volfiniune  28892  sbcaltop  30533  bj-sbeqALT  31252  csbdif  31470  phpreu  31633  finixpnum  31634  ptrest  31643  poimirlem23  31667  poimirlem24  31668  poimirlem25  31669  poimirlem26  31670  poimirlem27  31671  poimirlem28  31672  mbfposadd  31692  itgabsnc  31715  ftc1cnnclem  31719  ftc2nc  31730  fsumshftd  32232  fsumshftdOLD  32233  riotasv2s  32239  cdleme31sn  33656  cdleme31sn1  33657  cdleme31se2  33659  cdleme32fva  33713  cdleme42b  33754  hlhilset  35214  mzpsubst  35299  rabdiophlem2  35354  elnn0rabdioph  35355  dvdsrabdioph  35362  fphpd  35368  monotuz  35495  oddcomabszz  35498  aomclem6  35623  flcidc  35739  csbcog  35880  csbingOLD  36855  fsumcnf  36982  sumsnd  36987  elabrexg  37010  fiiuncl  37048  disjf1  37080  disjrnmpt2  37086  disjinfi  37091  iuneqfzuzlem  37166  fsumclf  37220  fsumsplitf  37221  fsummulc1f  37222  sumsnf  37223  fsumnncl  37225  fsumsplit1  37226  fsumf1of  37228  fsumiunss  37229  fprodexp  37246  fprodabs2  37247  mccllem  37249  fprodcncf  37351  dvmptmulf  37381  dvnmptdivc  37382  dvmptfprod  37389  iblsplitf  37416  fourierdlem86  37624  fourierdlem112  37650  sge0f1o  37758  sge0lempt  37786  sge0iunmptlemfi  37789  sge0iunmptlemre  37791  sge0iunmpt  37794  meadjiun  37813  csbafv12g  38029  csbaovg  38072  fsummsndifre  38415  fsumsplitsndif  38416  fsummmodsndifre  38417  fsummmodsnunz  38418  opeliun2xp  38874  dmmpt2ssx2  38878