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

Theorem eleq2s 2748
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 2722 . 2 (𝐴𝐶𝐴𝐵)
3 eleq2s.1 . 2 (𝐴𝐵𝜑)
42, 3sylbi 207 1 (𝐴𝐶𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wcel 2030
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-clel 2647
This theorem is referenced by:  elrabi  3391  epelg  5059  elxpi  5164  optocl  5229  eldmeldmressn  5475  predel  5735  fveqdmss  6394  oprabv  6745  elmpt2cl  6918  el2mpt2csbcl  7295  bropopvvv  7300  bropfvvvv  7302  ressuppss  7359  mpt2xeldm  7382  mpt2xopn0yelv  7384  mpt2xopxnop0  7386  tfr2a  7536  rdgseg  7563  2oconcl  7628  ecexr  7792  ectocld  7857  ecoptocl  7880  brecop2  7884  eroveu  7885  mapsnconst  7945  mapfienlem1  8351  mapfienlem2  8352  mapfienlem3  8353  cantnflem2  8625  r1sucg  8670  r1suc  8671  acnrcl  8903  dfac5lem4  8987  fin23lem29  9201  fin23lem30  9202  axcclem  9317  alephval2  9432  0tsk  9615  0nsr  9938  peano2nn  11070  uzssz  11745  peano2uzs  11780  uzsupss  11818  fzssnn  12423  prednn0  12502  fzossnn0  12538  fldiv4p1lem1div2  12676  ltweuz  12800  fzennn  12807  ser1const  12897  expp1  12907  facnn  13102  facp1  13105  bcpasc  13148  hashfzo0  13255  ccatval2  13396  ccatass  13406  swrd00  13463  swrd0  13480  wrdeqs1cat  13520  splfv2a  13553  revccat  13561  rexuz3  14132  rexanuz2  14133  r19.2uz  14135  rexuzre  14136  cau4  14140  caubnd2  14141  climrlim2  14322  climshft2  14357  climaddc1  14409  climmulc2  14411  climsubc1  14412  climsubc2  14413  climlec2  14433  isercoll2  14443  climsup  14444  climcau  14445  caurcvg  14451  caurcvg2  14452  caucvg  14453  caucvgb  14454  iseraltlem1  14456  iseralt  14459  binomlem  14605  isumshft  14615  cvgrat  14659  clim2div  14665  ntrivcvg  14673  ntrivcvgtail  14676  fprodntriv  14716  fprodeq0  14749  fprodefsum  14869  pwp1fsum  15161  3prm  15453  phicl2  15520  phibndlem  15522  dfphi2  15526  crth  15530  vdwap0  15727  prmlem1a  15860  xpscfv  16269  xpsfeq  16271  oppccofval  16423  homarcl2  16732  arwrcl  16741  pleval2i  17011  letsr  17274  gsumws1  17423  mulgpropd  17631  psgnunilem2  17961  psgnprfval  17987  gexid  18042  efgmnvl  18173  efgrcl  18174  efgsval  18190  efgs1  18194  efgs1b  18195  frgpuptinv  18230  frgpup3lem  18236  lt6abl  18342  eldprd  18449  isunit  18703  isirred  18745  abvrcl  18869  islss  18983  lbsss  19125  lbssp  19127  lbsind  19128  mpfrcl  19566  psr1basf  19619  coe1tm  19691  ply1frcl  19731  cssi  20076  thlle  20089  islbs4  20219  mavmulsolcl  20405  marepvcl  20423  1marepvmarrepid  20429  mdet0pr  20446  m2detleiblem1  20478  cramerimplem1  20537  cramerlem1  20541  chpscmat  20695  chpscmatgsumbin  20697  chpscmatgsummon  20698  ptpjpre1  21422  fin1aufil  21783  lmflf  21856  tsmsfbas  21978  xpsxmetlem  22231  xpsmet  22234  metustsym  22407  iscmet3lem3  23134  iscmet3lem1  23135  iscmet3lem2  23136  iscmet3  23137  rrxmvallem  23233  volsup  23370  opnmblALT  23417  itg1val  23495  tdeglem2  23866  ulmcaulem  24193  ulmcau  24194  ulmss  24196  pserdvlem2  24227  eff1olem  24339  logdmnrp  24432  dvlog2lem  24443  logtayl  24451  cxpcn3lem  24533  atancl  24653  atanval  24656  chp1  24938  ppiublem2  24973  lgsdir2lem2  25096  lgsdir2lem3  25097  lgsquadlem2  25151  2lgslem1b  25162  rplogsumlem1  25218  rplogsumlem2  25219  pntlemj  25337  1vgrex  25927  edglnl  26083  usgredg2v  26164  umgrres1lem  26247  upgrres1  26250  nbupgrres  26310  clwlkwlk  26727  wwlksnextproplem1  26872  wwlksnextproplem2  26873  wwlksnextproplem3  26874  rusgrnumwwlkb0  26938  clwlkclwwlklem2a4  26963  eleclclwwlknlem1  27025  eleclclwwlknlem2  27026  erclwwlkneqlen  27032  erclwwlknref  27033  erclwwlknsym  27034  erclwwlkntr  27035  hashecclwwlkn1  27041  umgrhashecclwwlk  27042  clwlksf1clwwlk  27056  frgrnbnb  27273  frgrwopreglem4  27295  frgrwopreglem5  27301  frgrwopreg  27303  vciOLD  27544  axhcompl-zf  27983  mayete3i  28715  pj3lem1  29193  fzto1stfv1  29979  fzto1st  29981  fzto1stinvn  29982  psgnfzto1st  29983  submat1n  29999  xrge0mulc1cn  30115  fiunelros  30365  elmbfmvol2  30457  fibp1  30591  rrvsum  30644  ballotlemfmpn  30684  reprsuc  30821  bnj529  30937  bnj923  30964  bnj570  31101  bnj594  31108  bnj1173  31196  bnj1256  31209  bnj1259  31210  bnj1296  31215  bnj1498  31255  subfacp1lem1  31287  kur14lem7  31320  mvrsval  31528  mvrsfpw  31529  mrsubcv  31533  mrsubccat  31541  msubff  31553  msrid  31568  msubvrs  31583  mppsval  31595  divcnvlin  31744  iprodefisumlem  31752  iprodefisum  31753  faclimlem1  31755  onsucsuccmpi  32567  bj-inftyexpidisj  33227  bj-ccinftydisj  33230  bj-elccinfty  33231  finixpnum  33524  poimirlem5  33544  poimirlem6  33545  poimirlem7  33546  poimirlem8  33547  poimirlem9  33548  poimirlem10  33549  poimirlem11  33550  poimirlem12  33551  poimirlem13  33552  poimirlem14  33553  poimirlem15  33554  poimirlem16  33555  poimirlem17  33556  poimirlem18  33557  poimirlem19  33558  poimirlem20  33559  poimirlem21  33560  poimirlem22  33561  poimirlem29  33568  poimirlem30  33569  broucube  33573  volsupnfl  33584  dvasin  33626  dvacos  33627  sdclem2  33668  fdc  33671  heiborlem4  33743  heiborlem6  33745  smgrpismgmOLD  33791  mndoissmgrpOLD  33797  mndoisexid  33798  rngoueqz  33869  drngoi  33880  jm2.23  37880  wepwsolem  37929  trclfvdecomr  38337  binomcxplemdvbinom  38869  binomcxplemnotnn0  38872  ssfiunibd  39837  climinf  40156  stoweidlem15  40550  fourierdlem66  40707  etransclem37  40806  smflimsuplem8  41354  eldmressn  41524  afvres  41573  ndmaovrcl  41605  pfx00  41709  pfx0  41710  fmtnofz04prm  41814  31prm  41837  sprsymrelfv  42069  2zrngamnd  42266  2zrngacmnd  42267  2zrngagrp  42268  2zrngALT  42273  2zrngnmlid  42274  2zrngnmlid2  42276  fldhmsubc  42409  fldhmsubcALTV  42427  lincvalsng  42530  snlindsntor  42585  lincresunit3lem2  42594  lincresunit3  42595  ldepsnlinc  42622  nn0sumshdiglemA  42738  nn0sumshdiglemB  42739
  Copyright terms: Public domain W3C validator