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

Theorem eleq2s 2705
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 2679 . 2 (𝐴𝐶𝐴𝐵)
3 eleq2s.1 . 2 (𝐴𝐵𝜑)
42, 3sylbi 205 1 (𝐴𝐶𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wcel 1976
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-cleq 2602  df-clel 2605
This theorem is referenced by:  elrabi  3327  epelg  4940  elxpi  5044  optocl  5108  eldmeldmressn  5347  predel  5600  fveqdmss  6247  oprabv  6579  elmpt2cl  6751  el2mpt2csbcl  7114  bropopvvv  7119  bropfvvvv  7121  ressuppss  7178  mpt2xeldm  7201  mpt2xopn0yelv  7203  mpt2xopxnop0  7205  tfr2a  7355  rdgseg  7382  2oconcl  7447  ecexr  7611  ectocld  7678  ecoptocl  7701  brecop2  7705  eroveu  7706  mapsnconst  7766  mapfienlem1  8170  mapfienlem2  8171  mapfienlem3  8172  cantnflem2  8447  r1sucg  8492  r1suc  8493  acnrcl  8725  dfac5lem4  8809  fin23lem29  9023  fin23lem30  9024  axcclem  9139  alephval2  9250  0tsk  9433  0nsr  9756  peano2nn  10879  uzssz  11539  peano2uzs  11574  uzsupss  11612  fzssnn  12211  prednn0  12287  fzossnn0  12323  fldiv4p1lem1div2  12453  ltweuz  12577  fzennn  12584  ser1const  12674  expp1  12684  facnn  12879  facp1  12882  bcpasc  12925  hashfzo0  13029  ccatval2  13161  ccatass  13170  swrd00  13216  swrd0  13232  wrdeqs1cat  13272  splfv2a  13304  revccat  13312  rexuz3  13882  rexanuz2  13883  r19.2uz  13885  rexuzre  13886  cau4  13890  caubnd2  13891  climrlim2  14072  climshft2  14107  climaddc1  14159  climmulc2  14161  climsubc1  14162  climsubc2  14163  climlec2  14183  isercoll2  14193  climsup  14194  climcau  14195  caurcvg  14201  caurcvg2  14202  caucvg  14203  caucvgb  14204  iseraltlem1  14206  iseralt  14209  binomlem  14346  isumshft  14356  cvgrat  14400  clim2div  14406  ntrivcvg  14414  ntrivcvgtail  14417  fprodntriv  14457  fprodeq0  14490  fprodefsum  14610  pwp1fsum  14898  3prm  15190  phicl2  15257  phibndlem  15259  dfphi2  15263  crth  15267  vdwap0  15464  prmlem1a  15597  xpscfv  15991  xpsfeq  15993  oppccofval  16145  homarcl2  16454  arwrcl  16463  pleval2i  16733  letsr  16996  gsumws1  17145  mulgpropd  17353  psgnunilem2  17684  psgnprfval  17710  gexid  17765  efgmnvl  17896  efgrcl  17897  efgsval  17913  efgs1  17917  efgs1b  17918  frgpuptinv  17953  frgpup3lem  17959  lt6abl  18065  eldprd  18172  isunit  18426  isirred  18468  abvrcl  18590  islss  18702  lbsss  18844  lbssp  18846  lbsind  18847  mpfrcl  19285  psr1basf  19338  coe1tm  19410  ply1frcl  19450  cssi  19789  thlle  19802  islbs4  19932  mavmulsolcl  20118  marepvcl  20136  1marepvmarrepid  20142  mdet0pr  20159  m2detleiblem1  20191  cramerimplem1  20250  cramerlem1  20254  chpscmat  20408  chpscmatgsumbin  20410  chpscmatgsummon  20411  ptpjpre1  21126  fin1aufil  21488  lmflf  21561  tsmsfbas  21683  xpsxmetlem  21935  xpsmet  21938  metustsym  22111  iscmet3lem3  22814  iscmet3lem1  22815  iscmet3lem2  22816  iscmet3  22817  rrxmvallem  22912  volsup  23048  opnmblALT  23094  itg1val  23173  tdeglem2  23542  ulmcaulem  23869  ulmcau  23870  ulmss  23872  pserdvlem2  23903  eff1olem  24015  logdmnrp  24104  dvlog2lem  24115  logtayl  24123  cxpcn3lem  24205  atancl  24325  atanval  24328  chp1  24610  ppiublem2  24645  lgsdir2lem2  24768  lgsdir2lem3  24769  lgsquadlem2  24823  2lgslem1b  24834  rplogsumlem1  24890  rplogsumlem2  24891  pntlemj  25009  uhgrac  25600  usgraidx2v  25688  nbgraf1olem3  25738  nbgraf1olem5  25740  wwlkextproplem1  26035  wwlkextproplem2  26036  wwlkextproplem3  26037  clwwlknprop  26066  clwlkisclwwlklem2a4  26078  eleclclwwlknlem1  26111  eleclclwwlknlem2  26112  erclwwlkneqlen  26118  erclwwlknref  26119  erclwwlknsym  26120  erclwwlkntr  26121  clwlkf1clwwlk  26143  2wlkonot3v  26168  2spthonot3v  26169  frgrawopreglem4  26340  frgrawopreg  26342  vciOLD  26569  axhcompl-zf  27045  mayete3i  27777  pj3lem1  28255  fzto1stfv1  28988  fzto1st  28990  fzto1stinvn  28991  psgnfzto1st  28992  submat1n  29005  xrge0mulc1cn  29121  fiunelros  29370  elmbfmvol2  29462  fibp1  29596  rrvsum  29649  ballotlemfmpn  29689  bnj529  29871  bnj923  29898  bnj570  30035  bnj594  30042  bnj1173  30130  bnj1256  30143  bnj1259  30144  bnj1296  30149  bnj1498  30189  subfacp1lem1  30221  kur14lem7  30254  mvrsval  30462  mvrsfpw  30463  mrsubcv  30467  mrsubccat  30475  msubff  30487  msrid  30502  msubvrs  30517  mppsval  30529  divcnvlin  30677  iprodefisumlem  30685  iprodefisum  30686  faclimlem1  30688  onsucsuccmpi  31418  bj-inftyexpidisj  32077  bj-ccinftydisj  32080  bj-elccinfty  32081  finixpnum  32367  poimirlem5  32387  poimirlem6  32388  poimirlem7  32389  poimirlem8  32390  poimirlem9  32391  poimirlem10  32392  poimirlem11  32393  poimirlem12  32394  poimirlem13  32395  poimirlem14  32396  poimirlem15  32397  poimirlem16  32398  poimirlem17  32399  poimirlem18  32400  poimirlem19  32401  poimirlem20  32402  poimirlem21  32403  poimirlem22  32404  poimirlem29  32411  poimirlem30  32412  broucube  32416  volsupnfl  32427  dvasin  32469  dvacos  32470  sdclem2  32511  fdc  32514  heiborlem4  32586  heiborlem6  32588  smgrpismgmOLD  32634  mndoissmgrpOLD  32640  mndoisexid  32641  rngoueqz  32712  drngoi  32723  jm2.23  36384  wepwsolem  36433  trclfvdecomr  36842  binomcxplemdvbinom  37377  binomcxplemnotnn0  37380  ssfiunibd  38267  climinf  38477  stoweidlem15  38712  fourierdlem66  38869  etransclem37  38968  eldmressn  39656  afvres  39706  ndmaovrcl  39738  fmtnofz04prm  39832  31prm  39855  pfx00  40052  pfx0  40053  1vgrex  40237  usgredg2v  40456  umgrres1lem  40531  upgrres1  40534  nbupgrres  40594  wwlksnextproplem1  41117  wwlksnextproplem2  41118  wwlksnextproplem3  41119  rusgrnumwwlkb0  41176  clwlkclwwlklem2a4  41208  eleclclwwlksnlem1  41247  eleclclwwlksnlem2  41248  erclwwlksneqlen  41254  erclwwlksnref  41255  erclwwlksnsym  41256  erclwwlksntr  41257  hashecclwwlksn1  41263  umgrhashecclwwlk  41264  clwlksf1clwwlk  41278  frgrnbnb  41465  frgrwopreglem4  41486  frgrwopreg  41488  2zrngamnd  41733  2zrngacmnd  41734  2zrngagrp  41735  2zrngALT  41740  2zrngnmlid  41741  2zrngnmlid2  41743  fldhmsubc  41878  fldhmsubcALTV  41897  lincvalsng  42001  snlindsntor  42056  lincresunit3lem2  42065  lincresunit3  42066  ldepsnlinc  42093  nn0sumshdiglemA  42213  nn0sumshdiglemB  42214
  Copyright terms: Public domain W3C validator