MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  csbeq1a Structured version   Visualization version   GIF version

Theorem csbeq1a 3867
Description: Equality theorem for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
Assertion
Ref Expression
csbeq1a (𝑥 = 𝐴𝐵 = 𝐴 / 𝑥𝐵)

Proof of Theorem csbeq1a
StepHypRef Expression
1 csbid 3866 . 2 𝑥 / 𝑥𝐵 = 𝐵
2 csbeq1 3856 . 2 (𝑥 = 𝐴𝑥 / 𝑥𝐵 = 𝐴 / 𝑥𝐵)
31, 2eqtr3id 2790 1 (𝑥 = 𝐴𝐵 = 𝐴 / 𝑥𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  csb 3853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-12 2171  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-sbc 3738  df-csb 3854
This theorem is referenced by:  csbhypf  3882  csbiebt  3883  cbvrabcsfw  3897  cbvralcsf  3898  cbvreucsf  3900  cbvrabcsf  3901  rspc2vd  3904  sbcnestgfw  4376  sbcnestgf  4381  csbun  4396  csbin  4397  csbdif  4483  csbif  4541  disjors  5084  invdisjrabw  5088  invdisjrab  5089  disjxiun  5100  disjxun  5101  sbcbr123  5157  eusvnf  5345  reusv2lem4  5354  reusv2  5356  moop2  5457  iunopeqop  5476  pofun  5561  opeliunxp  5697  elrnmpt1  5911  resmptf  5991  csbima12  6029  csbcog  6247  fvmpt2f  6946  fvmpts  6948  fvmptdf  6951  fvmpt2i  6955  fvmptex  6959  fmptco  7071  fmptcof  7072  fmptcos  7073  elabrex  7186  fliftfuns  7255  riotaeqimp  7336  csbov123  7395  ovmpos  7499  fvmpopr2d  7512  ofmpteq  7635  csbopeq1a  7978  mpomptsx  7992  dmmpossx  7994  fmpox  7995  el2mpocsbcl  8013  offval22  8016  ovmptss  8021  fmpoco  8023  mpoxeldm  8138  mpocurryd  8196  mpocurryvald  8197  fvmpocurryd  8198  eqerlem  8678  qliftfuns  8739  mptelixpg  8869  boxcutc  8875  xpf1o  9079  iunfi  9280  wdom2d  9512  ixpiunwdom  9522  hsmexlem2  10359  ac6c4  10413  iundom2g  10472  seqof2  13958  rlimcld2  15452  sumeq2ii  15570  summolem3  15591  summolem2a  15592  zsum  15595  fsum  15597  sumss2  15603  fsumcvg2  15604  fsumclf  15615  fsumzcl2  15616  fsumsplitf  15619  sumsnf  15620  fsumsplit1  15622  sumsns  15627  fsummsnunz  15631  fsumsplitsnun  15632  fsum2dlem  15647  fsumcnv  15650  fsumcom2  15651  fsumshftm  15658  fsum0diag2  15660  fsum00  15675  fsumabs  15678  fsumrlim  15688  fsumo1  15689  o1fsum  15690  fsumiun  15698  infcvgaux1i  15734  prodeq2ii  15788  prodmolem3  15808  prodmolem2a  15809  zprod  15812  fprod  15816  fprodntriv  15817  prodss  15822  fprodser  15824  fprodcllemf  15833  prodsn  15837  prodsnf  15839  fprodm1s  15845  fprodp1s  15846  prodsns  15847  fprodabs  15849  fprodn0  15854  fprod2dlem  15855  fprodcnv  15858  fprodcom2  15859  fproddivf  15862  fprodsplitf  15863  fprodsplit1f  15865  fprodle  15871  fprodmodd  15872  fprodefsum  15969  sumeven  16261  sumodd  16262  pcmpt  16756  pcmptdvds  16758  natpropd  17857  fucpropd  17858  gsummpt1n0  19733  gsumcom2  19743  gsummptnn0fz  19754  dprd2d2  19814  psrass1lemOLD  21327  psrass1lem  21330  mpfrcl  21479  coe1fzgsumdlem  21656  gsumply1eq  21660  evl1gsumdlem  21706  mdetralt2  21942  mdetunilem2  21946  madugsum  21976  fiuncmp  22739  ptcld  22948  ptcldmpt  22949  ptclsg  22950  elmptrab  23162  prdsdsf  23704  prdsxmet  23706  fsumcn  24217  fsum2cn  24218  ovolfiniun  24849  ovoliunlem3  24852  ovoliun  24853  ovoliun2  24854  ovoliunnul  24855  finiunmbl  24892  volfiniun  24895  iundisj  24896  iundisj2  24897  iunmbl  24901  iunmbl2  24905  itgss3  25163  itgfsum  25175  itgabs  25183  limciun  25242  dvmptfsum  25323  dvfsumle  25369  dvfsumabs  25371  dvfsumlem1  25374  dvfsumlem2  25375  dvfsumlem3  25376  dvfsumlem4  25377  dvfsumrlim  25379  dvfsumrlim2  25380  dvfsum2  25382  itgsubstlem  25396  itgsubst  25397  rlimcnp2  26300  fsumdvdscom  26518  fsumdvdsmul  26528  fsumvma  26545  dchrisumlema  26820  dchrisumlem2  26822  dchrisumlem3  26823  ifeqeqx  31350  disjorsf  31384  disjabrex  31386  disjabrexf  31387  iundisjf  31393  iundisj2f  31394  disjunsn  31398  suppss2f  31439  2ndresdju  31451  fmptdF  31458  fmptcof2  31459  acunirnmpt2f  31463  aciunf1lem  31464  funcnv4mpt  31471  f1od2  31521  iundisjfi  31582  iundisj2fi  31583  fsumiunle  31608  gsummpt2co  31773  gsumpart  31780  gsumvsca1  31944  gsumvsca2  31945  rmfsupp2  31958  esumpfinvalf  32544  esum2dlem  32560  esumiun  32562  fiunelros  32642  measiun  32686  voliune  32697  volfiniune  32698  sbcaltop  34533  bj-sbeqALT  35334  rdgssun  35816  finxpreclem2  35828  phpreu  36029  finixpnum  36030  ptrest  36044  poimirlem23  36068  poimirlem24  36069  poimirlem25  36070  poimirlem26  36071  poimirlem27  36072  poimirlem28  36073  mbfposadd  36092  itgabsnc  36114  ftc1cnnclem  36116  ftc2nc  36127  fsumshftd  37381  riotasv2s  37387  cdleme31sn  38810  cdleme31sn1  38811  cdleme31se2  38813  cdleme32fva  38867  cdleme42b  38908  hlhilset  40364  mzpsubst  41009  rabdiophlem2  41063  elnn0rabdioph  41064  dvdsrabdioph  41071  fphpd  41077  monotuz  41203  oddcomabszz  41206  aomclem6  41324  flcidc  41439  fsumcnf  43168  sumsnd  43173  elabrexg  43191  fiiuncl  43215  eliin2f  43256  disjf1  43337  disjrnmpt2  43343  disjinfi  43348  fmptf  43401  fmptff  43435  iuneqfzuzlem  43504  supxrleubrnmptf  43622  fsummulc1f  43744  fsumnncl  43745  fsumf1of  43747  fsumiunss  43748  fsumreclf  43749  fsumlessf  43750  fsumsermpt  43752  fprodexp  43767  fprodabs2  43768  mccllem  43770  fprodcnlem  43772  fprodcn  43773  climsubmpt  43833  climeldmeqmpt  43841  climfveqmpt  43844  climfveqmpt3  43855  climeldmeqmpt3  43862  climinf2mpt  43887  climinfmpt  43888  limsupequzmptf  43904  fprodcncf  44073  dvmptmulf  44110  dvnmptdivc  44111  dvmptfprod  44118  iblsplitf  44143  fourierdlem86  44365  fourierdlem112  44391  sge0f1o  44555  sge0lempt  44583  sge0iunmptlemfi  44586  sge0iunmptlemre  44588  sge0iunmpt  44591  sge0ltfirpmpt2  44599  sge0isummpt2  44605  sge0xaddlem2  44607  sge0xadd  44608  meadjiun  44639  hoimbl2  44838  vonhoire  44845  vonn0ioo2  44863  vonn0icc2  44865  csbafv12g  45301  csbaovg  45344  csbafv212g  45383  fsummsndifre  45496  fsumsplitsndif  45497  fsummmodsndifre  45498  fsummmodsnunz  45499  opeliun2xp  46340  dmmpossx2  46344
  Copyright terms: Public domain W3C validator