Theorem csbeq1a 3542

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

Syntax hints:   -> wi 4   = wceq 1483   [_csb 3533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-sbc 3436  df-csb 3534

This theorem is referenced by:  csbhypf  3552  csbiebt  3553  cbvralcsf  3565  cbvreucsf  3567  cbvrabcsf  3568  sbcnestgf  3995  csbun  4009  csbin  4010  csbif  4138  disjors  4635  invdisjrab  4639  disjxiun  4649  disjxiunOLD  4650  disjxun  4651  sbcbr123  4706  eusvnf  4861  reusv2lem4  4872  reusv2  4874  moop2  4966  iunopeqop  4981  pofun  5051  opeliunxp  5170  elrnmpt1  5374  resmptf  5451  csbima12  5483  fvmpt2f  6283  fvmpts  6285  fvmpt2i  6290  fvmptex  6294  fmptco  6396  fmptcof  6397  fmptcos  6398  elabrex  6501  fliftfuns  6564  riotaeqimp  6634  csbov123  6687  ovmpt2s  6784  ofmpteq  6916  csbopeq1a  7221  mpt2mptsx  7233  dmmpt2ssx  7235  fmpt2x  7236  el2mpt2csbcl  7250  offval22  7253  ovmptss  7258  fmpt2co  7260  mpt2xeldm  7337  mpt2curryd  7395  mpt2curryvald  7396  fvmpt2curryd  7397  eqerlem  7776  qliftfuns  7834  mptelixpg  7945  boxcutc  7951  xpf1o  8122  iunfi  8254  wdom2d  8485  ixpiunwdom  8496  hsmexlem2  9249  ac6num  9301  ac6c4  9303  iundom2g  9362  seqof2  12859  rlimcld2  14309  sumeq2ii  14423  summolem3  14445  summolem2a  14446  zsum  14449  fsum  14451  sumss2  14457  fsumcvg2  14458  fsumzcl2  14469  fsumsplitf  14472  sumsnf  14473  sumsn  14475  sumsns  14479  fsummsnunz  14483  fsumsplitsnun  14484  fsummsnunzOLD  14485  fsumsplitsnunOLD  14486  fsum2dlem  14501  fsumcnv  14504  fsumcom2  14505  fsumcom2OLD  14506  fsumshftm  14513  fsum0diag2  14515  fsum00  14530  fsumabs  14533  fsumrlim  14543  fsumo1  14544  o1fsum  14545  fsumiun  14553  infcvgaux1i  14589  prodeq2ii  14643  prodmolem3  14663  prodmolem2a  14664  zprod  14667  fprod  14671  fprodntriv  14672  prodss  14677  fprodser  14679  fprodcllemf  14688  prodsn  14692  prodsnf  14694  fprodm1s  14700  fprodp1s  14701  prodsns  14702  fprodabs  14704  fprodn0  14709  fprod2dlem  14710  fprodcnv  14713  fprodcom2  14714  fprodcom2OLD  14715  fproddivf  14718  fprodsplitf  14719  fprodsplit1f  14721  fprodle  14727  fprodmodd  14728  fprodefsum  14825  sumeven  15110  sumodd  15111  pcmpt  15596  pcmptdvds  15598  natpropd  16636  fucpropd  16637  gsummpt1n0  18364  gsumcom2  18374  gsummptnn0fz  18382  dprd2d2  18443  psrass1lem  19377  mpfrcl  19518  coe1fzgsumdlem  19671  gsumply1eq  19675  evl1gsumdlem  19720  mdetralt2  20415  mdetunilem2  20419  madugsum  20449  fiuncmp  21207  ptcld  21416  ptcldmpt  21417  ptclsg  21418  elmptrab  21630  prdsdsf  22172  prdsxmet  22174  fsumcn  22673  fsum2cn  22674  ovolfiniun  23269  ovoliunlem3  23272  ovoliun  23273  ovoliun2  23274  ovoliunnul  23275  finiunmbl  23312  volfiniun  23315  iundisj  23316  iundisj2  23317  iunmbl  23321  iunmbl2  23325  itgss3  23581  itgfsum  23593  itgabs  23601  limciun  23658  dvmptfsum  23738  dvfsumle  23784  dvfsumabs  23786  dvfsumlem1  23789  dvfsumlem2  23790  dvfsumlem3  23791  dvfsumlem4  23792  dvfsumrlim  23794  dvfsumrlim2  23795  dvfsum2  23797  itgsubstlem  23811  itgsubst  23812  rlimcnp2  24693  fsumdvdscom  24911  fsumdvdsmul  24921  fsumvma  24938  dchrisumlema  25177  dchrisumlem2  25179  dchrisumlem3  25180  rspc2vd  27129  ifeqeqx  29361  disjorsf  29393  disjabrex  29395  disjabrexf  29396  iundisjf  29402  iundisj2f  29403  disjunsn  29407  suppss2f  29439  fmptdF  29456  fmptcof2  29457  acunirnmpt2f  29461  aciunf1lem  29462  funcnv4mpt  29470  iundisjfi  29555  iundisj2fi  29556  fsumiunle  29575  gsummpt2co  29780  gsumvsca1  29782  gsumvsca2  29783  esumpfinvalf  30138  esum2dlem  30154  esumiun  30156  fiunelros  30237  measiun  30281  voliune  30292  volfiniune  30293  sbcaltop  32088  bj-sbeqALT  32895  csbdif  33171  finxpreclem2  33227  phpreu  33393  finixpnum  33394  ptrest  33408  poimirlem23  33432  poimirlem24  33433  poimirlem25  33434  poimirlem26  33435  poimirlem27  33436  poimirlem28  33437  mbfposadd  33457  itgabsnc  33479  ftc1cnnclem  33483  ftc2nc  33494  fsumshftd  34237  fsumshftdOLD  34238  riotasv2s  34244  cdleme31sn  35668  cdleme31sn1  35669  cdleme31se2  35671  cdleme32fva  35725  cdleme42b  35766  hlhilset  37226  mzpsubst  37311  rabdiophlem2  37366  elnn0rabdioph  37367  dvdsrabdioph  37374  fphpd  37380  monotuz  37506  oddcomabszz  37509  aomclem6  37629  flcidc  37744  csbcog  37941  csbingOLD  39054  fsumcnf  39180  sumsnd  39185  elabrexg  39206  fiiuncl  39234  eliin2f  39287  disjf1  39369  disjrnmpt2  39375  disjinfi  39380  fmptf  39448  iuneqfzuzlem  39550  supxrleubrnmptf  39680  fsumclf  39801  fsummulc1f  39802  fsumnncl  39803  fsumsplit1  39804  fsumf1of  39806  fsumiunss  39807  fsumreclf  39808  fsumlessf  39809  fsumsermpt  39811  fprodexp  39826  fprodabs2  39827  mccllem  39829  fprodcnlem  39831  fprodcn  39832  climsubmpt  39892  climeldmeqmpt  39900  climfveqmpt  39903  climfveqmpt3  39914  climeldmeqmpt3  39921  climinf2mpt  39946  climinfmpt  39947  limsupequzmptf  39963  fprodcncf  40114  dvmptmulf  40152  dvnmptdivc  40153  dvmptfprod  40160  iblsplitf  40186  fourierdlem86  40409  fourierdlem112  40435  sge0f1o  40599  sge0lempt  40627  sge0iunmptlemfi  40630  sge0iunmptlemre  40632  sge0iunmpt  40635  sge0ltfirpmpt2  40643  sge0isummpt2  40649  sge0xaddlem2  40651  sge0xadd  40652  meadjiun  40683  hoimbl2  40879  vonhoire  40886  vonn0ioo2  40904  vonn0icc2  40906  csbafv12g  41217  csbaovg  41260  fsummsndifre  41342  fsumsplitsndif  41343  fsummmodsndifre  41344  fsummmodsnunz  41345  opeliun2xp  42111  dmmpt2ssx2  42115