MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eleq2s Unicode version

Theorem eleq2s 2565
Description: Substitution of equal classes into a membership antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypotheses
Ref Expression
eleq2s.1
eleq2s.2
Assertion
Ref Expression
eleq2s

Proof of Theorem eleq2s
StepHypRef Expression
1 eleq2s.2 . . 3
21eleq2i 2535 . 2
3 eleq2s.1 . 2
42, 3sylbi 195 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818
This theorem is referenced by:  elrabi  3254  epelg  4797  elxpi  5020  optocl  5081  eldmeldmressn  5319  fveqdmss  6026  oprabv  6345  elmpt2cl  6517  bropopvvv  6880  ressuppss  6938  mpt2xopn0yelv  6960  mpt2xopxnop0  6962  tfr2a  7083  rdgseg  7107  2oconcl  7172  ecexr  7335  ectocld  7397  ecoptocl  7420  brecop2  7424  eroveu  7425  mapsnconst  7484  mapfienlem1  7884  mapfienlem2  7885  mapfienlem3  7886  cantnflem2  8130  r1sucg  8208  r1suc  8209  acnrcl  8444  dfac5lem4  8528  fin23lem29  8742  fin23lem30  8743  axcclem  8858  alephval2  8968  0tsk  9154  0nsr  9477  peano2nn  10573  uzssz  11129  peano2uzs  11164  uzsupss  11203  fzossnn0  11856  ltweuz  12072  fzennn  12078  ser1const  12163  expp1  12173  facnn  12355  facp1  12358  bcpasc  12399  hashfzo0  12488  ccatval2  12596  ccatass  12605  eqs1  12621  swrd00  12645  swrdid  12652  swrd0  12658  wrdeqcats1  12699  wrdeqs1cat  12700  splfv2a  12732  revccat  12740  rexuz3  13181  rexanuz2  13182  r19.2uz  13184  rexuzre  13185  cau4  13189  caubnd2  13190  climrlim2  13370  climshft2  13405  climaddc1  13457  climmulc2  13459  climsubc1  13460  climsubc2  13461  climlec2  13481  isercoll2  13491  climsup  13492  climcau  13493  caurcvg  13499  caurcvg2  13500  caucvg  13501  caucvgb  13502  iseraltlem1  13504  iseralt  13507  binomlem  13641  isumshft  13651  cvgrat  13692  clim2div  13698  ntrivcvg  13706  ntrivcvgtail  13709  fprodntriv  13749  fprodeq0  13779  fprodefsum  13830  3prm  14234  phicl2  14298  phibndlem  14300  dfphi2  14304  crt  14308  vdwap0  14494  prmlem1a  14592  xpscfv  14959  xpsfeq  14961  oppccofval  15111  homarcl2  15362  arwrcl  15371  pleval2i  15594  letsr  15857  gsumws1  16007  mulgpropd  16175  psgnunilem2  16520  psgnprfval  16546  gexid  16601  efgmnvl  16732  efgrcl  16733  efgsval  16749  efgs1  16753  efgs1b  16754  frgpuptinv  16789  frgpup3lem  16795  lt6abl  16897  eldprd  17035  eldprdOLD  17037  isunit  17306  isirred  17348  abvrcl  17470  islss  17581  lbsss  17723  lbssp  17725  lbsind  17726  mpfrcl  18187  psr1basf  18240  coe1tm  18314  ply1frcl  18355  cssi  18715  thlle  18728  islbs4  18867  mavmulsolcl  19053  marepvcl  19071  1marepvmarrepid  19077  mdet0pr  19094  m2detleiblem1  19126  cramerimplem1  19185  cramerlem1  19189  chpscmat  19343  chpscmatgsumbin  19345  chpscmatgsummon  19346  ptpjpre1  20072  fin1aufil  20433  lmflf  20506  tsmsfbas  20626  xpsxmetlem  20882  xpsmet  20885  metustsymOLD  21064  metustsym  21065  iscmet3lem3  21729  iscmet3lem1  21730  iscmet3lem2  21731  iscmet3  21732  rrxmvallem  21831  volsup  21966  opnmblALT  22012  itg1val  22090  tdeglem2  22459  ulmcaulem  22789  ulmcau  22790  ulmss  22792  pserdvlem2  22823  eff1olem  22935  logdmnrp  23022  dvlog2lem  23033  logtayl  23041  cxpcn3lem  23121  atancl  23212  atanval  23215  chp1  23441  ppiublem2  23478  lgsdir2lem2  23599  lgsdir2lem3  23600  lgsquadlem2  23630  rplogsumlem1  23669  rplogsumlem2  23670  pntlemj  23788  uhgrac  24305  usgraidx2v  24393  nbgraf1olem3  24443  nbgraf1olem5  24445  wwlkextproplem1  24741  wwlkextproplem2  24742  wwlkextproplem3  24743  clwwlknprop  24772  clwlkisclwwlklem2a4  24784  eleclclwwlknlem1  24817  eleclclwwlknlem2  24818  erclwwlkneqlen  24824  erclwwlknref  24825  erclwwlknsym  24826  erclwwlkntr  24827  clwlkf1clwwlk  24850  2wlkonot3v  24875  2spthonot3v  24876  frgrawopreglem4  25047  frgrawopreg  25049  gxnn0suc  25266  smgrpismgmOLD  25334  smgrpisass  25335  mndoissmgrpOLD  25341  mndoisexid  25342  drngoi  25409  rngoueqz  25432  vci  25441  axhcompl-zf  25915  mayete3i  26646  pj3lem1  27125  fzssnn  27595  xrge0mulc1cn  27923  elmbfmvol2  28238  fibp1  28340  rrvsum  28393  ballotlemfmpn  28433  subfacp1lem1  28623  kur14lem7  28656  mvrsval  28865  mvrsfpw  28866  mrsubcv  28870  mrsubccat  28878  msubff  28890  msrid  28905  msubvrs  28920  mppsval  28932  divcnvlin  29118  iprodefisumlem  29123  iprodefisum  29124  faclimlem1  29168  predel  29263  prednn0  29282  onsucsuccmpi  29908  finixpnum  30038  volsupnfl  30059  dvasin  30103  dvacos  30104  sdclem2  30235  fdc  30238  heiborlem4  30310  heiborlem6  30312  jm2.23  30938  wepwsolem  30987  binomcxplemdvbinom  31258  binomcxplemnotnn0  31261  ssfiunibd  31509  climinf  31612  stoweidlem15  31797  fourierdlem66  31955  etransclem37  32054  eldmressn  32208  afvres  32257  ndmaovrcl  32289  usgresvm1  32443  usgresvm1ALT  32447  2zrngamnd  32747  2zrngacmnd  32748  2zrngagrp  32749  2zrngALT  32754  2zrngnmlid  32755  2zrngnmlid2  32757  fldhmsubc  32892  fldhmsubcOLD  32911  lincvalsng  33017  snlindsntor  33072  lincresunit3lem2  33081  lincresunit3  33082  ldepsnlinc  33109  bnj529  33798  bnj923  33826  bnj570  33963  bnj594  33970  bnj1173  34058  bnj1256  34071  bnj1259  34072  bnj1296  34077  bnj1498  34117  bj-inftyexpidisj  34613  bj-ccinftydisj  34616  bj-elccinfty  34617
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-cleq 2449  df-clel 2452
  Copyright terms: Public domain W3C validator