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

Theorem eleq2s 2388
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 2360 . 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 1632    e. wcel 1696
This theorem is referenced by:  epelg  4322  elxpi  4721  optocl  4780  elmpt2cl  6077  tfr2a  6427  rdgseg  6451  2oconcl  6518  ecexr  6681  ectocld  6742  ecoptocl  6764  brecop2  6768  eroveu  6769  mapsnconst  6829  cantnflem2  7408  r1sucg  7457  r1suc  7458  acnrcl  7685  dfac5lem4  7769  fin23lem29  7983  fin23lem30  7984  axcclem  8099  alephval2  8210  0tsk  8393  0nsr  8717  peano2nn  9774  uzssz  10263  peano2uzs  10289  uzsupss  10326  ltweuz  11040  fzennn  11046  ser1const  11118  expp1  11126  facnn  11306  facp1  11309  bcn0  11339  bcpasc  11349  hashfzo0  11400  ccatval2  11448  ccatass  11452  eqs1  11463  swrd00  11467  swrdid  11474  splfv2a  11487  wrdeqcats1  11490  wrdeqs1cat  11491  revccat  11500  rexuz3  11848  rexanuz2  11849  r19.2uz  11851  rexuzre  11852  cau4  11856  caubnd2  11857  climrlim2  12037  climshft2  12072  climaddc1  12124  climmulc2  12126  climsubc1  12127  climsubc2  12128  climlec2  12148  isercoll2  12158  climsup  12159  climcau  12160  caurcvg  12165  caurcvg2  12166  caucvg  12167  caucvgb  12168  iseraltlem1  12170  iseralt  12173  binomlem  12303  isumshft  12314  cvgrat  12355  3prm  12791  phicl2  12852  phibndlem  12854  dfphi2  12858  crt  12862  vdwap0  13039  prmlem1a  13124  xpscfv  13480  xpsfeq  13482  oppccofval  13635  homarcl2  13883  arwrcl  13892  pleval2i  14114  letsr  14365  gsumws1  14478  mulgpropd  14616  gexid  14908  efgmnvl  15039  efgrcl  15040  efgsval  15056  efgs1  15060  efgs1b  15061  frgpuptinv  15096  frgpup3lem  15102  lt6abl  15197  eldprd  15255  isunit  15455  isirred  15497  abvrcl  15602  islss  15708  lbsss  15846  lbssp  15848  lbsind  15849  psr1basf  16297  coe1tm  16365  cssi  16600  thlle  16613  ptpjpre1  17282  fin1aufil  17643  lmflf  17716  tsmsfbas  17826  xpsxmetlem  17959  xpsmet  17962  iscmet3lem3  18732  iscmet3lem1  18733  iscmet3lem2  18734  iscmet3  18735  volsup  18929  opnmblALT  18974  itg1val  19054  mpfrcl  19418  tdeglem2  19463  ulmcaulem  19787  ulmcau  19788  ulmss  19790  pserdvlem2  19820  eff1olem  19926  logdmnrp  20004  dvlog2lem  20015  logtayl  20023  cxpcn3lem  20103  atancl  20193  atanval  20196  chp1  20421  ppiublem2  20458  lgsdir2lem2  20579  lgsdir2lem3  20580  lgsquadlem2  20610  rplogsumlem1  20649  rplogsumlem2  20650  pntlemj  20768  gxnn0suc  20947  smgrpismgm  21015  smgrpisass  21016  mndoissmgrp  21022  mndoisexid  21023  drngoi  21090  rngoueqz  21113  vci  21120  axhcompl-zf  21594  mayete3i  22323  pj3lem1  22802  xrge0mulc1cn  23338  lmxrge0  23390  subfacp1lem1  23725  kur14lem7  23758  faclim  24126  predel  24254  prednn0  24273  onsucsuccmpi  24954  dstr  25274  seqzp2  25458  com2i  25519  fldi  25530  vri  25595  intopcoaconlem3  25642  intrr  25802  intvconlem1  25806  algi  25830  0ded  25860  0catOLD  25861  indcls2  26099  pgapspf2  26156  sdclem2  26555  fdc  26558  heiborlem4  26641  heiborlem6  26643  jm2.23  27192  wepwsolem  27241  islbs4  27405  psgnunilem2  27521  climinf  27835  stoweidlem15  27867  eldmressn  28087  afvres  28140  ndmaovrcl  28172  mpt2xopn0yelv  28195  mpt2xopxnop0  28197  nbgrael  28275  trlonprop  28341  bnj529  29086  bnj923  29114  bnj570  29253  bnj594  29260  bnj1173  29348  bnj1256  29361  bnj1259  29362  bnj1296  29367  bnj1498  29407
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-cleq 2289  df-clel 2292
  Copyright terms: Public domain W3C validator