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

Theorem eleq2s 2375
Description: Substitution of equal classes into a membership antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypotheses
Ref Expression
eleq2s.1  |-  ( A  e.  B  ->  ph )
eleq2s.2  |-  C  =  B
Assertion
Ref Expression
eleq2s  |-  ( A  e.  C  ->  ph )

Proof of Theorem eleq2s
StepHypRef Expression
1 eleq2s.2 . . 3  |-  C  =  B
21eleq2i 2347 . 2  |-  ( A  e.  C  <->  A  e.  B )
3 eleq2s.1 . 2  |-  ( A  e.  B  ->  ph )
42, 3sylbi 187 1  |-  ( A  e.  C  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684
This theorem is referenced by:  epelg  4306  elxpi  4705  optocl  4764  elmpt2cl  6061  tfr2a  6411  rdgseg  6435  2oconcl  6502  ecexr  6665  ectocld  6726  ecoptocl  6748  brecop2  6752  eroveu  6753  mapsnconst  6813  cantnflem2  7392  r1sucg  7441  r1suc  7442  acnrcl  7669  dfac5lem4  7753  fin23lem29  7967  fin23lem30  7968  axcclem  8083  alephval2  8194  0tsk  8377  0nsr  8701  peano2nn  9758  uzssz  10247  peano2uzs  10273  uzsupss  10310  ltweuz  11024  fzennn  11030  ser1const  11102  expp1  11110  facnn  11290  facp1  11293  bcn0  11323  bcpasc  11333  hashfzo0  11384  ccatval2  11432  ccatass  11436  eqs1  11447  swrd00  11451  swrdid  11458  splfv2a  11471  wrdeqcats1  11474  wrdeqs1cat  11475  revccat  11484  rexuz3  11832  rexanuz2  11833  r19.2uz  11835  rexuzre  11836  cau4  11840  caubnd2  11841  climrlim2  12021  climshft2  12056  climaddc1  12108  climmulc2  12110  climsubc1  12111  climsubc2  12112  climlec2  12132  isercoll2  12142  climsup  12143  climcau  12144  caurcvg  12149  caurcvg2  12150  caucvg  12151  caucvgb  12152  iseraltlem1  12154  iseralt  12157  binomlem  12287  isumshft  12298  cvgrat  12339  3prm  12775  phicl2  12836  phibndlem  12838  dfphi2  12842  crt  12846  vdwap0  13023  prmlem1a  13108  xpscfv  13464  xpsfeq  13466  oppccofval  13619  homarcl2  13867  arwrcl  13876  pleval2i  14098  letsr  14349  gsumws1  14462  mulgpropd  14600  gexid  14892  efgmnvl  15023  efgrcl  15024  efgsval  15040  efgs1  15044  efgs1b  15045  frgpuptinv  15080  frgpup3lem  15086  lt6abl  15181  eldprd  15239  isunit  15439  isirred  15481  abvrcl  15586  islss  15692  lbsss  15830  lbssp  15832  lbsind  15833  psr1basf  16281  coe1tm  16349  cssi  16584  thlle  16597  ptpjpre1  17266  fin1aufil  17627  lmflf  17700  tsmsfbas  17810  xpsxmetlem  17943  xpsmet  17946  iscmet3lem3  18716  iscmet3lem1  18717  iscmet3lem2  18718  iscmet3  18719  volsup  18913  opnmblALT  18958  itg1val  19038  mpfrcl  19402  tdeglem2  19447  ulmcaulem  19771  ulmcau  19772  ulmss  19774  pserdvlem2  19804  eff1olem  19910  logdmnrp  19988  dvlog2lem  19999  logtayl  20007  cxpcn3lem  20087  atancl  20177  atanval  20180  chp1  20405  ppiublem2  20442  lgsdir2lem2  20563  lgsdir2lem3  20564  lgsquadlem2  20594  rplogsumlem1  20633  rplogsumlem2  20634  pntlemj  20752  gxnn0suc  20931  smgrpismgm  20999  smgrpisass  21000  mndoissmgrp  21006  mndoisexid  21007  drngoi  21074  rngoueqz  21097  vci  21104  axhcompl-zf  21578  mayete3i  22307  pj3lem1  22786  xrge0mulc1cn  23323  lmxrge0  23375  subfacp1lem1  23710  kur14lem7  23743  predel  24183  prednn0  24202  onsucsuccmpi  24882  dstr  25171  seqzp2  25355  com2i  25416  fldi  25427  vri  25492  intopcoaconlem3  25539  intrr  25699  intvconlem1  25703  algi  25727  0ded  25757  0catOLD  25758  indcls2  25996  pgapspf2  26053  sdclem2  26452  fdc  26455  heiborlem4  26538  heiborlem6  26540  jm2.23  27089  wepwsolem  27138  islbs4  27302  psgnunilem2  27418  climinf  27732  stoweidlem15  27764  eldmressn  27982  afvres  28034  ndmaovrcl  28064  mpt2xopn0yelv  28079  mpt2xopxnop0  28081  nbgrael  28141  bnj529  28770  bnj923  28798  bnj570  28937  bnj594  28944  bnj1173  29032  bnj1256  29045  bnj1259  29046  bnj1296  29051  bnj1498  29091
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-cleq 2276  df-clel 2279
  Copyright terms: Public domain W3C validator