Theorem csbeq1a 3859

Description: Equality theorem for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)

Assertion

Ref	Expression
csbeq1a	⊢ (𝑥 = 𝐴 → 𝐵 = ⦋𝐴 / 𝑥⦌𝐵)

Proof of Theorem csbeq1a

Step	Hyp	Ref	Expression
1		csbid 3858	. 2 ⊢ ⦋𝑥 / 𝑥⦌𝐵 = 𝐵
2		csbeq1 3848	. 2 ⊢ (𝑥 = 𝐴 → ⦋𝑥 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵)
3	1, 2	eqtr3id 2780	1 ⊢ (𝑥 = 𝐴 → 𝐵 = ⦋𝐴 / 𝑥⦌𝐵)

Syntax hints:   → wi 4   = wceq 1541  ⦋csb 3845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-12 2180  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-sbc 3737  df-csb 3846

This theorem is referenced by:  csbhypf  3873  csbiebt  3874  cbvrabcsfw  3886  cbvralcsf  3887  cbvreucsf  3889  cbvrabcsf  3890  rspc2vd  3893  sbcnestgfw  4370  sbcnestgf  4375  csbun  4390  csbin  4391  csbdif  4473  csbif  4532  disjors  5076  invdisjrab  5080  disjxiun  5090  disjxun  5091  sbcbr123  5147  eusvnf  5332  reusv2lem4  5341  reusv2  5343  moop2  5445  iunopeqop  5464  pofun  5545  opeliunxp  5686  opeliun2xp  5687  elrnmpt1  5905  resmptf  5993  csbima12  6033  csbcog  6250  fvmpt2f  6936  fvmpts  6938  fvmptdf  6941  fvmpt2i  6945  fvmptex  6949  fmptco  7068  fmptcof  7069  fmptcos  7070  elabrex  7182  elabrexg  7183  fliftfuns  7254  riotaeqimp  7335  csbov123  7396  ovmpos  7500  fvmpopr2d  7514  ofmpteq  7639  csbopeq1a  7988  mpomptsx  8002  dmmpossx  8004  fmpox  8005  el2mpocsbcl  8021  offval22  8024  ovmptss  8029  fmpoco  8031  mpoxeldm  8147  mpocurryd  8205  mpocurryvald  8206  fvmpocurryd  8207  eqerlem  8663  qliftfuns  8734  mptelixpg  8865  boxcutc  8871  xpf1o  9058  iunfi  9233  wdom2d  9472  ixpiunwdom  9482  hsmexlem2  10324  ac6c4  10378  iundom2g  10437  seqof2  13973  rlimcld2  15491  sumeq2ii  15606  summolem3  15627  summolem2a  15628  zsum  15631  fsum  15633  sumss2  15639  fsumcvg2  15640  fsumclf  15651  fsumzcl2  15652  fsumsplitf  15655  sumsnf  15656  fsumsplit1  15658  sumsns  15663  fsummsnunz  15667  fsumsplitsnun  15668  fsum2dlem  15683  fsumcnv  15686  fsumcom2  15687  fsumshftm  15694  fsum0diag2  15696  fsum00  15711  fsumabs  15714  fsumrlim  15724  fsumo1  15725  o1fsum  15726  fsumiun  15734  infcvgaux1i  15770  prodeq2ii  15824  prodmolem3  15846  prodmolem2a  15847  zprod  15850  fprod  15854  fprodntriv  15855  prodss  15860  fprodser  15862  fprodcllemf  15871  prodsn  15875  prodsnf  15877  fprodm1s  15883  fprodp1s  15884  prodsns  15885  fprodabs  15887  fprodn0  15892  fprod2dlem  15893  fprodcnv  15896  fprodcom2  15897  fproddivf  15900  fprodsplitf  15901  fprodsplit1f  15903  fprodle  15909  fprodmodd  15910  fprodefsum  16008  sumeven  16304  sumodd  16305  pcmpt  16810  pcmptdvds  16812  natpropd  17892  fucpropd  17893  gsummpt1n0  19883  gsumcom2  19893  gsummptnn0fz  19904  dprd2d2  19964  psrass1lem  21875  mpfrcl  22026  coe1fzgsumdlem  22224  gsumply1eq  22230  evl1gsumdlem  22277  mdetralt2  22530  mdetunilem2  22534  madugsum  22564  fiuncmp  23325  ptcld  23534  ptcldmpt  23535  ptclsg  23536  elmptrab  23748  prdsdsf  24288  prdsxmet  24290  fsumcn  24794  fsum2cn  24795  ovolfiniun  25435  ovoliunlem3  25438  ovoliun  25439  ovoliun2  25440  ovoliunnul  25441  finiunmbl  25478  volfiniun  25481  iundisj  25482  iundisj2  25483  iunmbl  25487  iunmbl2  25491  itgss3  25749  itgfsum  25761  itgabs  25769  limciun  25828  dvmptfsum  25912  dvfsumle  25959  dvfsumleOLD  25960  dvfsumabs  25962  dvfsumlem1  25965  dvfsumlem2  25966  dvfsumlem2OLD  25967  dvfsumlem3  25968  dvfsumlem4  25969  dvfsumrlim  25971  dvfsumrlim2  25972  dvfsum2  25974  itgsubstlem  25988  itgsubst  25989  rlimcnp2  26909  fsumdvdscom  27128  fsumdvdsmul  27138  fsumdvdsmulOLD  27140  fsumvma  27157  dchrisumlema  27432  dchrisumlem2  27434  dchrisumlem3  27435  ifeqeqx  32529  iunxpssiun1  32555  disjorsf  32567  disjabrex  32569  disjabrexf  32570  iundisjf  32576  iundisj2f  32577  disjunsn  32581  suppss2f  32627  2ndresdju  32638  fmptdF  32645  fmptcof2  32646  acunirnmpt2f  32650  aciunf1lem  32651  funcnv4mpt  32658  f1od2  32709  iundisjfi  32785  iundisj2fi  32786  fsumiunle  32819  gsummpt2co  33035  gsumpart  33044  gsumvsca1  33202  gsumvsca2  33203  rmfsupp2  33212  esumpfinvalf  34096  esum2dlem  34112  esumiun  34114  fiunelros  34194  measiun  34238  voliune  34249  volfiniune  34250  sbcaltop  36032  weiunpo  36516  weiunso  36517  weiunfr  36518  weiunse  36519  bj-sbeqALT  36951  rdgssun  37429  finxpreclem2  37441  phpreu  37650  finixpnum  37651  ptrest  37665  poimirlem23  37689  poimirlem24  37690  poimirlem25  37691  poimirlem26  37692  poimirlem27  37693  poimirlem28  37694  mbfposadd  37713  itgabsnc  37735  ftc1cnnclem  37737  ftc2nc  37748  fsumshftd  39057  riotasv2s  39063  cdleme31sn  40485  cdleme31sn1  40486  cdleme31se2  40488  cdleme32fva  40542  cdleme42b  40583  hlhilset  42039  evl1gprodd  42216  idomnnzgmulnz  42232  deg1gprod  42239  fmpocos  42333  mzpsubst  42846  rabdiophlem2  42900  elnn0rabdioph  42901  dvdsrabdioph  42908  fphpd  42914  monotuz  43039  oddcomabszz  43042  aomclem6  43157  flcidc  43268  fsumcnf  45123  sumsnd  45128  fiiuncl  45167  eliin2f  45206  disjf1  45285  disjrnmpt2  45290  disjinfi  45294  fmptf  45341  fmptff  45371  iuneqfzuzlem  45438  supxrleubrnmptf  45554  fsummulc1f  45676  fsumnncl  45677  fsumf1of  45679  fsumiunss  45680  fsumreclf  45681  fsumlessf  45682  fsumsermpt  45684  fprodexp  45699  fprodabs2  45700  mccllem  45702  fprodcnlem  45704  fprodcn  45705  climsubmpt  45763  climeldmeqmpt  45771  climfveqmpt  45774  climfveqmpt3  45785  climeldmeqmpt3  45792  climinf2mpt  45817  climinfmpt  45818  limsupequzmptf  45834  fprodcncf  46003  dvmptmulf  46040  dvnmptdivc  46041  dvmptfprod  46048  iblsplitf  46073  fourierdlem86  46295  fourierdlem112  46321  sge0f1o  46485  sge0lempt  46513  sge0iunmptlemfi  46516  sge0iunmptlemre  46518  sge0iunmpt  46521  sge0ltfirpmpt2  46529  sge0isummpt2  46535  sge0xaddlem2  46537  sge0xadd  46538  meadjiun  46569  hoimbl2  46768  vonhoire  46775  vonn0ioo2  46793  vonn0icc2  46795  csbafv12g  47242  csbaovg  47285  csbafv212g  47324  fsummsndifre  47477  fsumsplitsndif  47478  fsummmodsndifre  47479  fsummmodsnunz  47480  dmmpossx2  48442