Theorem csbeq1a 3444

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

Syntax hints:   -> wi 4   = wceq 1379   [_csb 3435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-sbc 3332  df-csb 3436

This theorem is referenced by:  csbhypf  3454  csbiebt  3455  cbvralcsf  3467  cbvreucsf  3469  cbvrabcsf  3470  sbcnestgf  3839  csbun  3857  csbungOLD  3858  csbin  3860  csbingOLD  3861  csbif  3989  csbifgOLD  3990  csbopg  4231  disjors  4433  disjxiun  4444  disjxun  4445  sbcbr123  4498  sbcbrgOLD  4499  eusvnf  4642  reusv2lem4  4651  reusv2  4653  moop2  4742  pofun  4816  opeliunxp  5051  elrnmpt1  5251  csbima12  5354  csbima12gOLD  5355  fvmpts  5952  fvmpt2i  5956  fvmptex  5960  fmptco  6054  fmptcof  6055  fmptcos  6056  elabrex  6143  fliftfuns  6200  csbov123  6315  csbovgOLD  6317  ovmpt2s  6410  ofmpteq  6542  csbopeq1a  6837  mpt2mptsx  6847  dmmpt2ssx  6849  fmpt2x  6850  offval22  6862  ovmptss  6864  fmpt2co  6866  mpt2curryd  6998  mpt2curryvald  6999  fvmpt2curryd  7000  eqerlem  7343  qliftfuns  7398  mptelixpg  7506  boxcutc  7512  xpf1o  7679  iunfi  7808  wdom2d  8006  ixpiunwdom  8017  hsmexlem2  8807  ac6num  8859  ac6c4  8861  iundom2g  8915  seqof2  12133  rlimcld2  13364  sumeq2w  13477  sumeq2ii  13478  summolem3  13499  summolem2a  13500  zsum  13503  fsum  13505  sumss2  13511  fsumcvg2  13512  fsumzcl2  13523  sumsn  13526  sumsns  13528  fsummsnunz  13532  fsumsplitsnun  13533  fsum2dlem  13548  fsumcnv  13551  fsumcom2  13552  fsumshftm  13559  fsum0diag2  13561  fsum00  13575  fsumabs  13578  fsumrlim  13588  fsumo1  13589  o1fsum  13590  fsumiun  13598  infcvgaux1i  13631  pcmpt  14270  pcmptdvds  14272  natpropd  15203  fucpropd  15204  gsummpt1n0  16795  gsumcom2  16806  gsummptnn0fz  16817  dprd2d2  16895  psrass1lem  17828  mpfrcl  17986  coe1fzgsumdlem  18142  gsumply1eq  18146  evl1gsumdlem  18191  mdetralt2  18906  mdetunilem2  18910  madugsum  18940  fiuncmp  19698  ptcld  19877  ptcldmpt  19878  ptclsg  19879  elmptrab  20091  prdsdsf  20633  prdsxmet  20635  fsumcn  21137  fsum2cn  21138  ovolfiniun  21675  ovoliunlem3  21678  ovoliun  21679  ovoliun2  21680  ovoliunnul  21681  finiunmbl  21717  volfiniun  21720  iundisj  21721  iundisj2  21722  iunmbl  21726  iunmbl2  21730  itgss3  21984  itgfsum  21996  itgabs  22004  limciun  22061  dvmptfsum  22139  dvfsumle  22185  dvfsumabs  22187  dvfsumlem1  22190  dvfsumlem2  22191  dvfsumlem3  22192  dvfsumlem4  22193  dvfsumrlim  22195  dvfsumrlim2  22196  dvfsum2  22198  itgsubstlem  22212  itgsubst  22213  rlimcnp2  23052  fsumdvdscom  23217  fsumdvdsmul  23227  fsumvma  23244  dchrisumlema  23429  dchrisumlem2  23431  dchrisumlem3  23432  ifeqeqx  27121  disjorsf  27142  disjabrex  27144  disjabrexf  27145  iundisjf  27149  iundisj2f  27150  disjunsn  27154  suppss2f  27178  fmptdF  27195  resmptf  27197  fvmpt2f  27198  fmptcof2  27202  funcnv4mpt  27212  iundisjfi  27297  iundisj2fi  27298  gsummpt2co  27462  gsumvsca1  27464  gsumvsca2  27465  esumpfinvalf  27750  measiun  27857  voliune  27869  volfiniune  27870  prodeq2w  28649  prodeq2ii  28650  prodmolem3  28670  prodmolem2a  28671  zprod  28674  fprod  28678  fprodntriv  28679  prodss  28684  fprodser  28686  prodsn  28697  fprodm1s  28704  fprodp1s  28705  prodsns  28706  fprodabs  28708  fprodefsum  28709  fprodn0  28714  fprod2dlem  28715  fprodcnv  28718  fprodcom2  28719  sbcaltop  29236  finixpnum  29643  ptrest  29653  mbfposadd  29667  itgabsnc  29689  ftc1cnnclem  29693  ftc2nc  29704  mzpsubst  30313  rabdiophlem2  30367  elnn0rabdioph  30368  dvdsrabdioph  30375  fphpd  30382  monotuz  30509  oddcomabszz  30512  aomclem6  30637  flcidc  30756  fsumcnf  31002  sumsnd  31007  elabrexg  31040  iblsplitf  31316  fourierdlem86  31521  fourierdlem112  31547  csbafv12g  31717  csbaovg  31760  fsummsndifre  31840  fsumsplitsndif  31841  fsummmodsndifre  31842  fsummmodsnunz  31843  opeliun2xp  32018  dmmpt2ssx2  32022  bj-sbeqALT  33566  fsumshftd  33772  fsumshftdOLD  33773  riotasv2s  33779  cdleme31sn  35194  cdleme31sn1  35195  cdleme31se2  35197  cdleme32fva  35251  cdleme42b  35292  hlhilset  36752