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

Theorem csbeq1a 3894
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 3893 . 2 𝑥 / 𝑥𝐵 = 𝐵
2 csbeq1 3883 . 2 (𝑥 = 𝐴𝑥 / 𝑥𝐵 = 𝐴 / 𝑥𝐵)
31, 2syl5eqr 2867 1 (𝑥 = 𝐴𝐵 = 𝐴 / 𝑥𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  csb 3880
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1531  df-ex 1772  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-sbc 3770  df-csb 3881
This theorem is referenced by:  csbhypf  3908  csbiebt  3909  cbvrabcsfw  3921  cbvralcsf  3922  cbvreucsf  3924  cbvrabcsf  3925  rspc2vd  3929  sbcnestgfw  4367  sbcnestgf  4372  csbun  4387  csbin  4388  csbif  4518  disjors  5038  invdisjrabw  5042  invdisjrab  5043  disjxiun  5054  disjxun  5055  sbcbr123  5111  eusvnf  5283  reusv2lem4  5292  reusv2  5294  moop2  5383  iunopeqop  5402  pofun  5484  opeliunxp  5612  elrnmpt1  5823  resmptf  5900  csbima12  5940  fvmpt2f  6762  fvmpts  6764  fvmpt2i  6770  fvmptex  6774  fmptco  6883  fmptcof  6884  fmptcos  6885  elabrex  6993  fliftfuns  7056  riotaeqimp  7129  csbov123  7187  ovmpos  7287  ofmpteq  7417  csbopeq1a  7738  mpomptsx  7751  dmmpossx  7753  fmpox  7754  el2mpocsbcl  7769  offval22  7772  ovmptss  7777  fmpoco  7779  mpoxeldm  7866  mpocurryd  7924  mpocurryvald  7925  fvmpocurryd  7926  eqerlem  8312  qliftfuns  8373  mptelixpg  8487  boxcutc  8493  xpf1o  8667  iunfi  8800  wdom2d  9032  ixpiunwdom  9043  hsmexlem2  9837  ac6c4  9891  iundom2g  9950  seqof2  13416  rlimcld2  14923  sumeq2ii  15038  summolem3  15059  summolem2a  15060  zsum  15063  fsum  15065  sumss2  15071  fsumcvg2  15072  fsumzcl2  15083  fsumsplitf  15086  sumsnf  15087  sumsns  15093  fsummsnunz  15097  fsumsplitsnun  15098  fsum2dlem  15113  fsumcnv  15116  fsumcom2  15117  fsumshftm  15124  fsum0diag2  15126  fsum00  15141  fsumabs  15144  fsumrlim  15154  fsumo1  15155  o1fsum  15156  fsumiun  15164  infcvgaux1i  15200  prodeq2ii  15255  prodmolem3  15275  prodmolem2a  15276  zprod  15279  fprod  15283  fprodntriv  15284  prodss  15289  fprodser  15291  fprodcllemf  15300  prodsn  15304  prodsnf  15306  fprodm1s  15312  fprodp1s  15313  prodsns  15314  fprodabs  15316  fprodn0  15321  fprod2dlem  15322  fprodcnv  15325  fprodcom2  15326  fproddivf  15329  fprodsplitf  15330  fprodsplit1f  15332  fprodle  15338  fprodmodd  15339  fprodefsum  15436  sumeven  15726  sumodd  15727  pcmpt  16216  pcmptdvds  16218  natpropd  17234  fucpropd  17235  gsummpt1n0  19014  gsumcom2  19024  gsummptnn0fz  19035  dprd2d2  19095  psrass1lem  20085  mpfrcl  20226  coe1fzgsumdlem  20397  gsumply1eq  20401  evl1gsumdlem  20447  mdetralt2  21146  mdetunilem2  21150  madugsum  21180  fiuncmp  21940  ptcld  22149  ptcldmpt  22150  ptclsg  22151  elmptrab  22363  prdsdsf  22904  prdsxmet  22906  fsumcn  23405  fsum2cn  23406  ovolfiniun  24029  ovoliunlem3  24032  ovoliun  24033  ovoliun2  24034  ovoliunnul  24035  finiunmbl  24072  volfiniun  24075  iundisj  24076  iundisj2  24077  iunmbl  24081  iunmbl2  24085  itgss3  24342  itgfsum  24354  itgabs  24362  limciun  24419  dvmptfsum  24499  dvfsumle  24545  dvfsumabs  24547  dvfsumlem1  24550  dvfsumlem2  24551  dvfsumlem3  24552  dvfsumlem4  24553  dvfsumrlim  24555  dvfsumrlim2  24556  dvfsum2  24558  itgsubstlem  24572  itgsubst  24573  rlimcnp2  25471  fsumdvdscom  25689  fsumdvdsmul  25699  fsumvma  25716  dchrisumlema  25991  dchrisumlem2  25993  dchrisumlem3  25994  ifeqeqx  30224  disjorsf  30258  disjabrex  30260  disjabrexf  30261  iundisjf  30267  iundisj2f  30268  disjunsn  30272  suppss2f  30312  fmptdF  30329  fmptcof2  30330  acunirnmpt2f  30334  aciunf1lem  30335  funcnv4mpt  30342  f1od2  30383  iundisjfi  30445  iundisj2fi  30446  fsumiunle  30472  gsummpt2co  30613  gsumvsca1  30781  gsumvsca2  30782  rmfsupp2  30793  esumpfinvalf  31234  esum2dlem  31250  esumiun  31252  fiunelros  31332  measiun  31376  voliune  31387  volfiniune  31388  sbcaltop  33339  bj-sbeqALT  34114  csbdif  34488  rdgssun  34541  finxpreclem2  34553  phpreu  34757  finixpnum  34758  ptrest  34772  poimirlem23  34796  poimirlem24  34797  poimirlem25  34798  poimirlem26  34799  poimirlem27  34800  poimirlem28  34801  mbfposadd  34820  itgabsnc  34842  ftc1cnnclem  34846  ftc2nc  34857  fsumshftd  35968  riotasv2s  35974  cdleme31sn  37396  cdleme31sn1  37397  cdleme31se2  37399  cdleme32fva  37453  cdleme42b  37494  hlhilset  38950  mzpsubst  39223  rabdiophlem2  39277  elnn0rabdioph  39278  dvdsrabdioph  39285  fphpd  39291  monotuz  39416  oddcomabszz  39419  aomclem6  39537  flcidc  39652  csbcog  39872  fsumcnf  41155  sumsnd  41160  elabrexg  41180  fiiuncl  41204  eliin2f  41247  disjf1  41319  disjrnmpt2  41325  disjinfi  41330  fmptf  41385  iuneqfzuzlem  41478  supxrleubrnmptf  41603  fsumclf  41726  fsummulc1f  41727  fsumnncl  41728  fsumsplit1  41729  fsumf1of  41731  fsumiunss  41732  fsumreclf  41733  fsumlessf  41734  fsumsermpt  41736  fprodexp  41751  fprodabs2  41752  mccllem  41754  fprodcnlem  41756  fprodcn  41757  climsubmpt  41817  climeldmeqmpt  41825  climfveqmpt  41828  climfveqmpt3  41839  climeldmeqmpt3  41846  climinf2mpt  41871  climinfmpt  41872  limsupequzmptf  41888  fprodcncf  42060  dvmptmulf  42098  dvnmptdivc  42099  dvmptfprod  42106  iblsplitf  42131  fourierdlem86  42354  fourierdlem112  42380  sge0f1o  42541  sge0lempt  42569  sge0iunmptlemfi  42572  sge0iunmptlemre  42574  sge0iunmpt  42577  sge0ltfirpmpt2  42585  sge0isummpt2  42591  sge0xaddlem2  42593  sge0xadd  42594  meadjiun  42625  hoimbl2  42824  vonhoire  42831  vonn0ioo2  42849  vonn0icc2  42851  csbafv12g  43213  csbaovg  43256  csbafv212g  43295  fsummsndifre  43409  fsumsplitsndif  43410  fsummmodsndifre  43411  fsummmodsnunz  43412  opeliun2xp  44309  dmmpossx2  44313
  Copyright terms: Public domain W3C validator