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

Theorem csbeq1a 3508
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 3507 . 2 𝑥 / 𝑥𝐵 = 𝐵
2 csbeq1 3502 . 2 (𝑥 = 𝐴𝑥 / 𝑥𝐵 = 𝐴 / 𝑥𝐵)
31, 2syl5eqr 2658 1 (𝑥 = 𝐴𝐵 = 𝐴 / 𝑥𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  csb 3499
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-sbc 3403  df-csb 3500
This theorem is referenced by:  csbhypf  3518  csbiebt  3519  cbvralcsf  3531  cbvreucsf  3533  cbvrabcsf  3534  sbcnestgf  3947  csbun  3961  csbin  3962  csbif  4088  disjors  4563  invdisjrab  4567  disjxiun  4574  disjxiunOLD  4575  disjxun  4576  sbcbr123  4631  eusvnf  4782  reusv2lem4  4793  reusv2  4795  moop2  4885  pofun  4965  opeliunxp  5083  elrnmpt1  5282  csbima12  5389  fvmpt2f  6177  fvmpts  6179  fvmpt2i  6184  fvmptex  6188  fmptco  6288  fmptcof  6289  fmptcos  6290  elabrex  6383  fliftfuns  6442  csbov123  6563  ovmpt2s  6660  ofmpteq  6792  csbopeq1a  7090  mpt2mptsx  7100  dmmpt2ssx  7102  fmpt2x  7103  el2mpt2csbcl  7115  offval22  7118  ovmptss  7123  fmpt2co  7125  mpt2xeldm  7202  mpt2curryd  7260  mpt2curryvald  7261  fvmpt2curryd  7262  eqerlem  7641  qliftfuns  7699  mptelixpg  7809  boxcutc  7815  xpf1o  7985  iunfi  8115  wdom2d  8346  ixpiunwdom  8357  hsmexlem2  9110  ac6num  9162  ac6c4  9164  iundom2g  9219  seqof2  12679  rlimcld2  14106  sumeq2ii  14220  summolem3  14241  summolem2a  14242  zsum  14245  fsum  14247  sumss2  14253  fsumcvg2  14254  fsumzcl2  14265  sumsn  14268  sumsns  14272  fsummsnunz  14276  fsumsplitsnun  14277  fsum2dlem  14292  fsumcnv  14295  fsumcom2  14296  fsumcom2OLD  14297  fsumshftm  14304  fsum0diag2  14306  fsum00  14320  fsumabs  14323  fsumrlim  14333  fsumo1  14334  o1fsum  14335  fsumiun  14343  infcvgaux1i  14377  prodeq2ii  14431  prodmolem3  14451  prodmolem2a  14452  zprod  14455  fprod  14459  fprodntriv  14460  prodss  14465  fprodser  14467  fprodcllemf  14476  prodsn  14480  prodsnf  14482  fprodm1s  14488  fprodp1s  14489  prodsns  14490  fprodabs  14492  fprodn0  14497  fprod2dlem  14498  fprodcnv  14501  fprodcom2  14502  fprodcom2OLD  14503  fproddivf  14506  fprodsplitf  14507  fprodsplit1f  14509  fprodle  14515  fprodmodd  14516  fprodefsum  14613  sumeven  14897  sumodd  14898  pcmpt  15383  pcmptdvds  15385  natpropd  16408  fucpropd  16409  gsummpt1n0  18136  gsumcom2  18146  gsummptnn0fz  18154  dprd2d2  18215  psrass1lem  19147  mpfrcl  19288  coe1fzgsumdlem  19441  gsumply1eq  19445  evl1gsumdlem  19490  mdetralt2  20182  mdetunilem2  20186  madugsum  20216  fiuncmp  20965  ptcld  21174  ptcldmpt  21175  ptclsg  21176  elmptrab  21388  prdsdsf  21930  prdsxmet  21932  fsumcn  22429  fsum2cn  22430  ovolfiniun  23021  ovoliunlem3  23024  ovoliun  23025  ovoliun2  23026  ovoliunnul  23027  finiunmbl  23064  volfiniun  23067  iundisj  23068  iundisj2  23069  iunmbl  23073  iunmbl2  23077  itgss3  23332  itgfsum  23344  itgabs  23352  limciun  23409  dvmptfsum  23487  dvfsumle  23533  dvfsumabs  23535  dvfsumlem1  23538  dvfsumlem2  23539  dvfsumlem3  23540  dvfsumlem4  23541  dvfsumrlim  23543  dvfsumrlim2  23544  dvfsum2  23546  itgsubstlem  23560  itgsubst  23561  rlimcnp2  24438  fsumdvdscom  24656  fsumdvdsmul  24666  fsumvma  24683  dchrisumlema  24922  dchrisumlem2  24924  dchrisumlem3  24925  ifeqeqx  28539  disjorsf  28569  disjabrex  28571  disjabrexf  28572  iundisjf  28578  iundisj2f  28579  disjunsn  28583  suppss2f  28613  fmptdF  28630  resmptf  28632  fmptcof2  28633  acunirnmpt2f  28637  aciunf1lem  28638  funcnv4mpt  28647  iundisjfi  28736  iundisj2fi  28737  gsummpt2co  28905  gsumvsca1  28907  gsumvsca2  28908  esumpfinvalf  29259  esum2dlem  29275  esumiun  29277  fiunelros  29358  measiun  29402  voliune  29413  volfiniune  29414  sbcaltop  31052  bj-sbeqALT  31881  csbdif  32141  finxpreclem2  32197  phpreu  32357  finixpnum  32358  ptrest  32372  poimirlem23  32396  poimirlem24  32397  poimirlem25  32398  poimirlem26  32399  poimirlem27  32400  poimirlem28  32401  mbfposadd  32421  itgabsnc  32443  ftc1cnnclem  32447  ftc2nc  32458  fsumshftd  33049  fsumshftdOLD  33050  riotasv2s  33056  cdleme31sn  34480  cdleme31sn1  34481  cdleme31se2  34483  cdleme32fva  34537  cdleme42b  34578  hlhilset  36038  mzpsubst  36123  rabdiophlem2  36178  elnn0rabdioph  36179  dvdsrabdioph  36186  fphpd  36192  monotuz  36318  oddcomabszz  36321  aomclem6  36441  flcidc  36557  csbcog  36754  csbingOLD  37870  fsumcnf  37997  sumsnd  38002  elabrexg  38023  fiiuncl  38053  eliin2f  38110  disjf1  38158  disjrnmpt2  38164  disjinfi  38169  iuneqfzuzlem  38285  fsumclf  38427  fsumsplitf  38428  fsummulc1f  38429  sumsnf  38430  fsumnncl  38432  fsumsplit1  38433  fsumf1of  38435  fsumiunss  38436  fsumreclf  38437  fsumlessf  38438  fsumsermpt  38440  fprodexp  38455  fprodabs2  38456  mccllem  38458  fprodcnlem  38460  fprodcn  38461  climsubmpt  38521  climeldmeqmpt  38529  climfveqmpt  38532  fprodcncf  38581  dvmptmulf  38621  dvnmptdivc  38622  dvmptfprod  38629  iblsplitf  38656  fourierdlem86  38879  fourierdlem112  38905  sge0f1o  39069  sge0lempt  39097  sge0iunmptlemfi  39100  sge0iunmptlemre  39102  sge0iunmpt  39105  sge0ltfirpmpt2  39113  sge0isummpt2  39119  sge0xaddlem2  39121  sge0xadd  39122  meadjiun  39153  hoimbl2  39349  vonhoire  39357  vonn0ioo2  39375  vonn0icc2  39377  csbafv12g  39661  csbaovg  39704  iunopeqop  40121  riotaeqimp  40155  fsummsndifre  40211  fsumsplitsndif  40212  fsummmodsndifre  40213  fsummmodsnunz  40214  rspc2vd  41429  opeliun2xp  41896  dmmpt2ssx2  41900
  Copyright terms: Public domain W3C validator