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

Theorem eleq2s 2706
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 2680 . 2 (𝐴𝐶𝐴𝐵)
3 eleq2s.1 . 2 (𝐴𝐵𝜑)
42, 3sylbi 206 1 (𝐴𝐶𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  wcel 1977
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-ext 2590
This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606
This theorem is referenced by:  elrabi  3328  epelg  4950  elxpi  5054  optocl  5118  eldmeldmressn  5360  predel  5614  fveqdmss  6262  oprabv  6601  elmpt2cl  6774  el2mpt2csbcl  7137  bropopvvv  7142  bropfvvvv  7144  ressuppss  7201  mpt2xeldm  7224  mpt2xopn0yelv  7226  mpt2xopxnop0  7228  tfr2a  7378  rdgseg  7405  2oconcl  7470  ecexr  7634  ectocld  7701  ecoptocl  7724  brecop2  7728  eroveu  7729  mapsnconst  7789  mapfienlem1  8193  mapfienlem2  8194  mapfienlem3  8195  cantnflem2  8470  r1sucg  8515  r1suc  8516  acnrcl  8748  dfac5lem4  8832  fin23lem29  9046  fin23lem30  9047  axcclem  9162  alephval2  9273  0tsk  9456  0nsr  9779  peano2nn  10909  uzssz  11583  peano2uzs  11618  uzsupss  11656  fzssnn  12256  prednn0  12332  fzossnn0  12368  fldiv4p1lem1div2  12498  ltweuz  12622  fzennn  12629  ser1const  12719  expp1  12729  facnn  12924  facp1  12927  bcpasc  12970  hashfzo0  13077  ccatval2  13215  ccatass  13224  swrd00  13270  swrd0  13286  wrdeqs1cat  13326  splfv2a  13358  revccat  13366  rexuz3  13936  rexanuz2  13937  r19.2uz  13939  rexuzre  13940  cau4  13944  caubnd2  13945  climrlim2  14126  climshft2  14161  climaddc1  14213  climmulc2  14215  climsubc1  14216  climsubc2  14217  climlec2  14237  isercoll2  14247  climsup  14248  climcau  14249  caurcvg  14255  caurcvg2  14256  caucvg  14257  caucvgb  14258  iseraltlem1  14260  iseralt  14263  binomlem  14400  isumshft  14410  cvgrat  14454  clim2div  14460  ntrivcvg  14468  ntrivcvgtail  14471  fprodntriv  14511  fprodeq0  14544  fprodefsum  14664  pwp1fsum  14952  3prm  15244  phicl2  15311  phibndlem  15313  dfphi2  15317  crth  15321  vdwap0  15518  prmlem1a  15651  xpscfv  16045  xpsfeq  16047  oppccofval  16199  homarcl2  16508  arwrcl  16517  pleval2i  16787  letsr  17050  gsumws1  17199  mulgpropd  17407  psgnunilem2  17738  psgnprfval  17764  gexid  17819  efgmnvl  17950  efgrcl  17951  efgsval  17967  efgs1  17971  efgs1b  17972  frgpuptinv  18007  frgpup3lem  18013  lt6abl  18119  eldprd  18226  isunit  18480  isirred  18522  abvrcl  18644  islss  18756  lbsss  18898  lbssp  18900  lbsind  18901  mpfrcl  19339  psr1basf  19392  coe1tm  19464  ply1frcl  19504  cssi  19847  thlle  19860  islbs4  19990  mavmulsolcl  20176  marepvcl  20194  1marepvmarrepid  20200  mdet0pr  20217  m2detleiblem1  20249  cramerimplem1  20308  cramerlem1  20312  chpscmat  20466  chpscmatgsumbin  20468  chpscmatgsummon  20469  ptpjpre1  21184  fin1aufil  21546  lmflf  21619  tsmsfbas  21741  xpsxmetlem  21994  xpsmet  21997  metustsym  22170  iscmet3lem3  22896  iscmet3lem1  22897  iscmet3lem2  22898  iscmet3  22899  rrxmvallem  22995  volsup  23131  opnmblALT  23177  itg1val  23256  tdeglem2  23625  ulmcaulem  23952  ulmcau  23953  ulmss  23955  pserdvlem2  23986  eff1olem  24098  logdmnrp  24187  dvlog2lem  24198  logtayl  24206  cxpcn3lem  24288  atancl  24408  atanval  24411  chp1  24693  ppiublem2  24728  lgsdir2lem2  24851  lgsdir2lem3  24852  lgsquadlem2  24906  2lgslem1b  24917  rplogsumlem1  24973  rplogsumlem2  24974  pntlemj  25092  1vgrex  25679  uhgrac  25834  usgraidx2v  25922  nbgraf1olem3  25972  nbgraf1olem5  25974  wwlkextproplem1  26269  wwlkextproplem2  26270  wwlkextproplem3  26271  clwwlknprop  26300  clwlkisclwwlklem2a4  26312  eleclclwwlknlem1  26345  eleclclwwlknlem2  26346  erclwwlkneqlen  26352  erclwwlknref  26353  erclwwlknsym  26354  erclwwlkntr  26355  clwlkf1clwwlk  26377  2wlkonot3v  26402  2spthonot3v  26403  frgrawopreglem4  26574  frgrawopreg  26576  vciOLD  26800  axhcompl-zf  27239  mayete3i  27971  pj3lem1  28449  fzto1stfv1  29182  fzto1st  29184  fzto1stinvn  29185  psgnfzto1st  29186  submat1n  29199  xrge0mulc1cn  29315  fiunelros  29564  elmbfmvol2  29656  fibp1  29790  rrvsum  29843  ballotlemfmpn  29883  bnj529  30065  bnj923  30092  bnj570  30229  bnj594  30236  bnj1173  30324  bnj1256  30337  bnj1259  30338  bnj1296  30343  bnj1498  30383  subfacp1lem1  30415  kur14lem7  30448  mvrsval  30656  mvrsfpw  30657  mrsubcv  30661  mrsubccat  30669  msubff  30681  msrid  30696  msubvrs  30711  mppsval  30723  divcnvlin  30871  iprodefisumlem  30879  iprodefisum  30880  faclimlem1  30882  onsucsuccmpi  31612  bj-inftyexpidisj  32274  bj-ccinftydisj  32277  bj-elccinfty  32278  finixpnum  32564  poimirlem5  32584  poimirlem6  32585  poimirlem7  32586  poimirlem8  32587  poimirlem9  32588  poimirlem10  32589  poimirlem11  32590  poimirlem12  32591  poimirlem13  32592  poimirlem14  32593  poimirlem15  32594  poimirlem16  32595  poimirlem17  32596  poimirlem18  32597  poimirlem19  32598  poimirlem20  32599  poimirlem21  32600  poimirlem22  32601  poimirlem29  32608  poimirlem30  32609  broucube  32613  volsupnfl  32624  dvasin  32666  dvacos  32667  sdclem2  32708  fdc  32711  heiborlem4  32783  heiborlem6  32785  smgrpismgmOLD  32831  mndoissmgrpOLD  32837  mndoisexid  32838  rngoueqz  32909  drngoi  32920  jm2.23  36581  wepwsolem  36630  trclfvdecomr  37039  binomcxplemdvbinom  37574  binomcxplemnotnn0  37577  ssfiunibd  38464  climinf  38673  stoweidlem15  38908  fourierdlem66  39065  etransclem37  39164  eldmressn  39852  afvres  39901  ndmaovrcl  39933  fmtnofz04prm  40027  31prm  40050  pfx00  40247  pfx0  40248  usgredg2v  40454  umgrres1lem  40529  upgrres1  40532  nbupgrres  40592  wwlksnextproplem1  41115  wwlksnextproplem2  41116  wwlksnextproplem3  41117  rusgrnumwwlkb0  41174  clwlkclwwlklem2a4  41206  eleclclwwlksnlem1  41245  eleclclwwlksnlem2  41246  erclwwlksneqlen  41252  erclwwlksnref  41253  erclwwlksnsym  41254  erclwwlksntr  41255  hashecclwwlksn1  41261  umgrhashecclwwlk  41262  clwlksf1clwwlk  41276  frgrnbnb  41463  frgrwopreglem4  41484  frgrwopreg  41486  2zrngamnd  41731  2zrngacmnd  41732  2zrngagrp  41733  2zrngALT  41738  2zrngnmlid  41739  2zrngnmlid2  41741  fldhmsubc  41876  fldhmsubcALTV  41895  lincvalsng  41999  snlindsntor  42054  lincresunit3lem2  42063  lincresunit3  42064  ldepsnlinc  42091  nn0sumshdiglemA  42211  nn0sumshdiglemB  42212
  Copyright terms: Public domain W3C validator