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

Theorem eleq2s 2716
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 2690 . 2 (𝐴𝐶𝐴𝐵)
3 eleq2s.1 . 2 (𝐴𝐵𝜑)
42, 3sylbi 207 1 (𝐴𝐶𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  wcel 1987
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-cleq 2614  df-clel 2617
This theorem is referenced by:  elrabi  3347  epelg  4996  elxpi  5100  optocl  5166  eldmeldmressn  5409  predel  5666  fveqdmss  6320  oprabv  6668  elmpt2cl  6841  el2mpt2csbcl  7210  bropopvvv  7215  bropfvvvv  7217  ressuppss  7274  mpt2xeldm  7297  mpt2xopn0yelv  7299  mpt2xopxnop0  7301  tfr2a  7451  rdgseg  7478  2oconcl  7543  ecexr  7707  ectocld  7774  ecoptocl  7797  brecop2  7801  eroveu  7802  mapsnconst  7863  mapfienlem1  8270  mapfienlem2  8271  mapfienlem3  8272  cantnflem2  8547  r1sucg  8592  r1suc  8593  acnrcl  8825  dfac5lem4  8909  fin23lem29  9123  fin23lem30  9124  axcclem  9239  alephval2  9354  0tsk  9537  0nsr  9860  peano2nn  10992  uzssz  11667  peano2uzs  11702  uzsupss  11740  fzssnn  12343  prednn0  12420  fzossnn0  12456  fldiv4p1lem1div2  12592  ltweuz  12716  fzennn  12723  ser1const  12813  expp1  12823  facnn  13018  facp1  13021  bcpasc  13064  hashfzo0  13173  ccatval2  13317  ccatass  13326  swrd00  13372  swrd0  13388  wrdeqs1cat  13428  splfv2a  13460  revccat  13468  rexuz3  14038  rexanuz2  14039  r19.2uz  14041  rexuzre  14042  cau4  14046  caubnd2  14047  climrlim2  14228  climshft2  14263  climaddc1  14315  climmulc2  14317  climsubc1  14318  climsubc2  14319  climlec2  14339  isercoll2  14349  climsup  14350  climcau  14351  caurcvg  14357  caurcvg2  14358  caucvg  14359  caucvgb  14360  iseraltlem1  14362  iseralt  14365  binomlem  14505  isumshft  14515  cvgrat  14559  clim2div  14565  ntrivcvg  14573  ntrivcvgtail  14576  fprodntriv  14616  fprodeq0  14649  fprodefsum  14769  pwp1fsum  15057  3prm  15349  phicl2  15416  phibndlem  15418  dfphi2  15422  crth  15426  vdwap0  15623  prmlem1a  15756  xpscfv  16162  xpsfeq  16164  oppccofval  16316  homarcl2  16625  arwrcl  16634  pleval2i  16904  letsr  17167  gsumws1  17316  mulgpropd  17524  psgnunilem2  17855  psgnprfval  17881  gexid  17936  efgmnvl  18067  efgrcl  18068  efgsval  18084  efgs1  18088  efgs1b  18089  frgpuptinv  18124  frgpup3lem  18130  lt6abl  18236  eldprd  18343  isunit  18597  isirred  18639  abvrcl  18761  islss  18875  lbsss  19017  lbssp  19019  lbsind  19020  mpfrcl  19458  psr1basf  19511  coe1tm  19583  ply1frcl  19623  cssi  19968  thlle  19981  islbs4  20111  mavmulsolcl  20297  marepvcl  20315  1marepvmarrepid  20321  mdet0pr  20338  m2detleiblem1  20370  cramerimplem1  20429  cramerlem1  20433  chpscmat  20587  chpscmatgsumbin  20589  chpscmatgsummon  20590  ptpjpre1  21314  fin1aufil  21676  lmflf  21749  tsmsfbas  21871  xpsxmetlem  22124  xpsmet  22127  metustsym  22300  iscmet3lem3  23028  iscmet3lem1  23029  iscmet3lem2  23030  iscmet3  23031  rrxmvallem  23127  volsup  23264  opnmblALT  23311  itg1val  23390  tdeglem2  23759  ulmcaulem  24086  ulmcau  24087  ulmss  24089  pserdvlem2  24120  eff1olem  24232  logdmnrp  24321  dvlog2lem  24332  logtayl  24340  cxpcn3lem  24422  atancl  24542  atanval  24545  chp1  24827  ppiublem2  24862  lgsdir2lem2  24985  lgsdir2lem3  24986  lgsquadlem2  25040  2lgslem1b  25051  rplogsumlem1  25107  rplogsumlem2  25108  pntlemj  25226  1vgrex  25816  usgredg2v  26046  umgrres1lem  26124  upgrres1  26127  nbupgrres  26187  clwlkwlk  26574  wwlksnextproplem1  26707  wwlksnextproplem2  26708  wwlksnextproplem3  26709  rusgrnumwwlkb0  26767  clwlkclwwlklem2a4  26799  eleclclwwlksnlem1  26838  eleclclwwlksnlem2  26839  erclwwlksneqlen  26845  erclwwlksnref  26846  erclwwlksnsym  26847  erclwwlksntr  26848  hashecclwwlksn1  26854  umgrhashecclwwlk  26855  clwlksf1clwwlk  26869  frgrnbnb  27055  frgrwopreglem4  27076  frgrwopreg  27078  vciOLD  27304  axhcompl-zf  27743  mayete3i  28475  pj3lem1  28953  fzto1stfv1  29678  fzto1st  29680  fzto1stinvn  29681  psgnfzto1st  29682  submat1n  29695  xrge0mulc1cn  29811  fiunelros  30060  elmbfmvol2  30152  fibp1  30286  rrvsum  30339  ballotlemfmpn  30379  breprsuc  30501  bnj529  30572  bnj923  30599  bnj570  30736  bnj594  30743  bnj1173  30831  bnj1256  30844  bnj1259  30845  bnj1296  30850  bnj1498  30890  subfacp1lem1  30922  kur14lem7  30955  mvrsval  31163  mvrsfpw  31164  mrsubcv  31168  mrsubccat  31176  msubff  31188  msrid  31203  msubvrs  31218  mppsval  31230  divcnvlin  31379  iprodefisumlem  31387  iprodefisum  31388  faclimlem1  31390  onsucsuccmpi  32137  bj-inftyexpidisj  32769  bj-ccinftydisj  32772  bj-elccinfty  32773  finixpnum  33065  poimirlem5  33085  poimirlem6  33086  poimirlem7  33087  poimirlem8  33088  poimirlem9  33089  poimirlem10  33090  poimirlem11  33091  poimirlem12  33092  poimirlem13  33093  poimirlem14  33094  poimirlem15  33095  poimirlem16  33096  poimirlem17  33097  poimirlem18  33098  poimirlem19  33099  poimirlem20  33100  poimirlem21  33101  poimirlem22  33102  poimirlem29  33109  poimirlem30  33110  broucube  33114  volsupnfl  33125  dvasin  33167  dvacos  33168  sdclem2  33209  fdc  33212  heiborlem4  33284  heiborlem6  33286  smgrpismgmOLD  33332  mndoissmgrpOLD  33338  mndoisexid  33339  rngoueqz  33410  drngoi  33421  jm2.23  37082  wepwsolem  37131  trclfvdecomr  37540  binomcxplemdvbinom  38073  binomcxplemnotnn0  38076  ssfiunibd  39022  climinf  39274  stoweidlem15  39569  fourierdlem66  39726  etransclem37  39825  smflimsuplem8  40370  eldmressn  40537  afvres  40586  ndmaovrcl  40618  pfx00  40713  pfx0  40714  fmtnofz04prm  40818  31prm  40841  sprsymrelfv  41062  2zrngamnd  41259  2zrngacmnd  41260  2zrngagrp  41261  2zrngALT  41266  2zrngnmlid  41267  2zrngnmlid2  41269  fldhmsubc  41402  fldhmsubcALTV  41420  lincvalsng  41523  snlindsntor  41578  lincresunit3lem2  41587  lincresunit3  41588  ldepsnlinc  41615  nn0sumshdiglemA  41735  nn0sumshdiglemB  41736
  Copyright terms: Public domain W3C validator