Theorem csbeq1a 3384

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

Syntax hints:   -> wi 4   = wceq 1455   [_csb 3375

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-sbc 3280  df-csb 3376

This theorem is referenced by:  csbhypf  3394  csbiebt  3395  cbvralcsf  3407  cbvreucsf  3409  cbvrabcsf  3410  sbcnestgf  3796  csbun  3810  csbin  3811  csbif  3943  csbopg  4198  disjors  4404  invdisjrab  4408  disjxiun  4415  disjxun  4416  sbcbr123  4470  eusvnf  4615  reusv2lem4  4624  reusv2  4626  moop2  4713  pofun  4793  opeliunxp  4908  elrnmpt1  5105  csbima12  5207  csbima12gOLD  5208  fvmpt2f  5977  fvmpts  5979  fvmpt2i  5984  fvmptex  5988  fmptco  6085  fmptcof  6086  fmptcos  6087  elabrex  6178  fliftfuns  6237  csbov123  6354  ovmpt2s  6452  ofmpteq  6582  csbopeq1a  6878  mpt2mptsx  6888  dmmpt2ssx  6890  fmpt2x  6891  offval22  6904  ovmptss  6909  fmpt2co  6911  mpt2xeldm  6989  mpt2curryd  7047  mpt2curryvald  7048  fvmpt2curryd  7049  eqerlem  7426  qliftfuns  7481  mptelixpg  7590  boxcutc  7596  xpf1o  7765  iunfi  7893  wdom2d  8126  ixpiunwdom  8137  hsmexlem2  8888  ac6num  8940  ac6c4  8942  iundom2g  8996  seqof2  12309  rlimcld2  13697  sumeq2ii  13814  summolem3  13835  summolem2a  13836  zsum  13839  fsum  13841  sumss2  13847  fsumcvg2  13848  fsumzcl2  13859  sumsn  13862  sumsns  13866  fsummsnunz  13870  fsumsplitsnun  13871  fsum2dlem  13886  fsumcnv  13889  fsumcom2  13890  fsumshftm  13897  fsum0diag2  13899  fsum00  13913  fsumabs  13916  fsumrlim  13926  fsumo1  13927  o1fsum  13928  fsumiun  13936  infcvgaux1i  13970  prodeq2ii  14022  prodmolem3  14042  prodmolem2a  14043  zprod  14046  fprod  14050  fprodntriv  14051  prodss  14056  fprodser  14058  fprodcllemf  14067  prodsn  14071  prodsnf  14073  fprodm1s  14079  fprodp1s  14080  prodsns  14081  fprodabs  14083  fprodn0  14088  fprod2dlem  14089  fprodcnv  14092  fprodcom2  14093  fproddivf  14096  fprodsplitf  14097  fprodsplit1f  14099  fprodle  14105  fprodefsum  14204  pcmpt  14892  pcmptdvds  14894  natpropd  15936  fucpropd  15937  gsummpt1n0  17652  gsumcom2  17662  gsummptnn0fz  17670  dprd2d2  17732  psrass1lem  18656  mpfrcl  18796  coe1fzgsumdlem  18950  gsumply1eq  18954  evl1gsumdlem  18999  mdetralt2  19689  mdetunilem2  19693  madugsum  19723  fiuncmp  20474  ptcld  20683  ptcldmpt  20684  ptclsg  20685  elmptrab  20897  prdsdsf  21437  prdsxmet  21439  fsumcn  21957  fsum2cn  21958  ovolfiniun  22509  ovoliunlem3  22512  ovoliun  22513  ovoliun2  22514  ovoliunnul  22515  finiunmbl  22553  volfiniun  22556  iundisj  22557  iundisj2  22558  iunmbl  22562  iunmbl2  22566  itgss3  22828  itgfsum  22840  itgabs  22848  limciun  22905  dvmptfsum  22983  dvfsumle  23029  dvfsumabs  23031  dvfsumlem1  23034  dvfsumlem2  23035  dvfsumlem3  23036  dvfsumlem4  23037  dvfsumrlim  23039  dvfsumrlim2  23040  dvfsum2  23042  itgsubstlem  23056  itgsubst  23057  rlimcnp2  23948  fsumdvdscom  24170  fsumdvdsmul  24180  fsumvma  24197  dchrisumlema  24382  dchrisumlem2  24384  dchrisumlem3  24385  ifeqeqx  28213  disjorsf  28244  disjabrex  28246  disjabrexf  28247  iundisjf  28253  iundisj2f  28254  disjunsn  28258  suppss2fOLD  28290  suppss2f  28291  fmptdF  28308  resmptf  28310  fmptcof2  28311  acunirnmpt2f  28315  aciunf1lem  28316  funcnv4mpt  28325  iundisjfi  28424  iundisj2fi  28425  gsummpt2co  28594  gsumvsca1  28596  gsumvsca2  28597  esumpfinvalf  28948  esum2dlem  28964  esumiun  28966  fiunelros  29047  measiun  29091  voliune  29102  volfiniune  29103  sbcaltop  30798  bj-sbeqALT  31548  csbdif  31772  finxpreclem2  31828  phpreu  31975  finixpnum  31976  ptrest  31985  poimirlem23  32009  poimirlem24  32010  poimirlem25  32011  poimirlem26  32012  poimirlem27  32013  poimirlem28  32014  mbfposadd  32034  itgabsnc  32057  ftc1cnnclem  32061  ftc2nc  32072  fsumshftd  32569  fsumshftdOLD  32570  riotasv2s  32576  cdleme31sn  33993  cdleme31sn1  33994  cdleme31se2  33996  cdleme32fva  34050  cdleme42b  34091  hlhilset  35551  mzpsubst  35636  rabdiophlem2  35691  elnn0rabdioph  35692  dvdsrabdioph  35699  fphpd  35705  monotuz  35835  oddcomabszz  35838  aomclem6  35963  flcidc  36086  csbcog  36287  csbingOLD  37256  fsumcnf  37383  sumsnd  37388  elabrexg  37410  fiiuncl  37445  disjf1  37511  disjrnmpt2  37517  disjinfi  37522  iuneqfzuzlem  37632  fsumclf  37730  fsumsplitf  37731  fsummulc1f  37732  sumsnf  37733  fsumnncl  37735  fsumsplit1  37736  fsumf1of  37738  fsumiunss  37739  fsumreclf  37740  fsumlessf  37741  fsumsermpt  37743  fprodexp  37760  fprodabs2  37761  mccllem  37763  fprodcncf  37865  dvmptmulf  37898  dvnmptdivc  37899  dvmptfprod  37906  iblsplitf  37933  fourierdlem86  38157  fourierdlem112  38183  sge0f1o  38327  sge0lempt  38355  sge0iunmptlemfi  38358  sge0iunmptlemre  38360  sge0iunmpt  38363  sge0ltfirpmpt2  38371  sge0isummpt2  38377  sge0xaddlem2  38379  sge0xadd  38380  meadjiun  38409  csbafv12g  38774  csbaovg  38817  iunopeqop  39141  riotaeqimp  39175  fsummsndifre  39233  fsumsplitsndif  39234  fsummmodsndifre  39235  fsummmodsnunz  39236  opeliun2xp  40483  dmmpt2ssx2  40487