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

Theorem eleq2s 2528
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 2500 . 2  |-  ( A  e.  C  <->  A  e.  B )
3 eleq2s.1 . 2  |-  ( A  e.  B  ->  ph )
42, 3sylbi 188 1  |-  ( A  e.  C  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    e. wcel 1725
This theorem is referenced by:  elrabi  3090  epelg  4495  elxpi  4894  optocl  4952  elmpt2cl  6288  bropopvvv  6426  mpt2xopn0yelv  6464  mpt2xopxnop0  6466  tfr2a  6656  rdgseg  6680  2oconcl  6747  ecexr  6910  ectocld  6971  ecoptocl  6994  brecop2  6998  eroveu  6999  mapsnconst  7059  cantnflem2  7646  r1sucg  7695  r1suc  7696  acnrcl  7923  dfac5lem4  8007  fin23lem29  8221  fin23lem30  8222  axcclem  8337  alephval2  8447  0tsk  8630  0nsr  8954  peano2nn  10012  uzssz  10505  peano2uzs  10531  uzsupss  10568  ltweuz  11301  fzennn  11307  ser1const  11379  expp1  11388  facnn  11568  facp1  11571  bcn0  11601  bcpasc  11612  hashfzo0  11695  ccatval2  11746  ccatass  11750  eqs1  11761  swrd00  11765  swrdid  11772  splfv2a  11785  wrdeqcats1  11788  wrdeqs1cat  11789  revccat  11798  rexuz3  12152  rexanuz2  12153  r19.2uz  12155  rexuzre  12156  cau4  12160  caubnd2  12161  climrlim2  12341  climshft2  12376  climaddc1  12428  climmulc2  12430  climsubc1  12431  climsubc2  12432  climlec2  12452  isercoll2  12462  climsup  12463  climcau  12464  caurcvg  12470  caurcvg2  12471  caucvg  12472  caucvgb  12473  iseraltlem1  12475  iseralt  12478  binomlem  12608  isumshft  12619  cvgrat  12660  3prm  13096  phicl2  13157  phibndlem  13159  dfphi2  13163  crt  13167  vdwap0  13344  prmlem1a  13429  xpscfv  13787  xpsfeq  13789  oppccofval  13942  homarcl2  14190  arwrcl  14199  pleval2i  14421  letsr  14672  gsumws1  14785  mulgpropd  14923  gexid  15215  efgmnvl  15346  efgrcl  15347  efgsval  15363  efgs1  15367  efgs1b  15368  frgpuptinv  15403  frgpup3lem  15409  lt6abl  15504  eldprd  15562  isunit  15762  isirred  15804  abvrcl  15909  islss  16011  lbsss  16149  lbssp  16151  lbsind  16152  psr1basf  16599  coe1tm  16665  cssi  16911  thlle  16924  ptpjpre1  17603  fin1aufil  17964  lmflf  18037  tsmsfbas  18157  xpsxmetlem  18409  xpsmet  18412  metustsymOLD  18591  metustsym  18592  iscmet3lem3  19243  iscmet3lem1  19244  iscmet3lem2  19245  iscmet3  19246  volsup  19450  opnmblALT  19495  itg1val  19575  mpfrcl  19939  tdeglem2  19984  ulmcaulem  20310  ulmcau  20311  ulmss  20313  pserdvlem2  20344  eff1olem  20450  logdmnrp  20532  dvlog2lem  20543  logtayl  20551  cxpcn3lem  20631  atancl  20721  atanval  20724  chp1  20950  ppiublem2  20987  lgsdir2lem2  21108  lgsdir2lem3  21109  lgsquadlem2  21139  rplogsumlem1  21178  rplogsumlem2  21179  pntlemj  21297  usgraidx2v  21412  nbgraf1olem3  21453  nbgraf1olem5  21455  gxnn0suc  21852  smgrpismgm  21920  smgrpisass  21921  mndoissmgrp  21927  mndoisexid  21928  drngoi  21995  rngoueqz  22018  vci  22027  axhcompl-zf  22501  mayete3i  23230  pj3lem1  23709  fzssnn  24147  xrge0mulc1cn  24327  elmbfmvol2  24617  rrvsum  24712  ballotlemfmpn  24752  subfacp1lem1  24865  kur14lem7  24898  divcnvlin  25212  clim2div  25217  ntrivcvg  25225  ntrivcvgtail  25228  fprodntriv  25268  fprodefsum  25298  fprodeq0  25299  iprodefisumlem  25317  iprodefisum  25318  faclimlem1  25362  predel  25458  prednn0  25477  onsucsuccmpi  26193  volsupnfl  26251  sdclem2  26446  fdc  26449  heiborlem4  26523  heiborlem6  26525  jm2.23  27067  wepwsolem  27116  islbs4  27279  psgnunilem2  27395  climinf  27708  stoweidlem15  27740  eldmressn  27960  afvres  28012  ndmaovrcl  28044  oprabv  28085  fzossnn0  28124  2wlkonot3v  28342  2spthonot3v  28343  frgrawopreglem4  28436  frgrawopreg  28438  bnj529  29109  bnj923  29137  bnj570  29276  bnj594  29283  bnj1173  29371  bnj1256  29384  bnj1259  29385  bnj1296  29390  bnj1498  29430
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-cleq 2429  df-clel 2432
  Copyright terms: Public domain W3C validator