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

Theorem syl6eqel 2475
Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
Hypotheses
Ref Expression
syl6eqel.1  |-  ( ph  ->  A  =  B )
syl6eqel.2  |-  B  e.  C
Assertion
Ref Expression
syl6eqel  |-  ( ph  ->  A  e.  C )

Proof of Theorem syl6eqel
StepHypRef Expression
1 syl6eqel.1 . 2  |-  ( ph  ->  A  =  B )
2 syl6eqel.2 . . 3  |-  B  e.  C
32a1i 11 . 2  |-  ( ph  ->  B  e.  C )
41, 3eqeltrd 2461 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1717
This theorem is referenced by:  syl6eqelr  2476  class2set  4308  snexALT  4326  snex  4346  prex  4347  onun2i  4637  unisn2  4651  soex  5259  iotaex  5375  fvrn0  5693  f0cli  5819  zfrep6  5907  elimdelov  6092  ndmovcl  6171  caovmo  6223  1st2ndb  6326  smofvon2  6554  tz7.44-2  6601  oesuclem  6705  omcl  6716  oecl  6717  nnmcl  6791  nnecl  6792  ixpexg  7022  resixpfo  7036  en1b  7111  xpsnen  7128  nnunifi  7294  xpfi  7314  oiexg  7437  hartogslem1  7444  noinfepOLD  7548  cantnfvalf  7553  cantnf0  7563  rankdmr1  7660  rankr1c  7680  numwdom  7873  alephon  7883  isfin5  8112  sdom2en01  8115  isf32lem9  8174  hsmexlem9  8238  iundom2g  8348  gchxpidm  8477  r1tskina  8590  tskmcl  8649  recmulnq  8774  recclnq  8776  genpelv  8810  un0mulcl  10186  znegcl  10245  zeo  10287  eqreznegel  10493  xnegcl  10731  ioorebas  10938  fzofi  11240  expcllem  11319  m1expcl2  11330  faclbnd4lem3  11513  bccl  11540  hasheq0  11571  hashrabrsn  11575  abs00bd  12023  iserge0  12381  sumrblem  12432  fsumcvg  12433  summolem2a  12436  zsum  12439  sumss  12445  fsumss  12446  fsumcvg2  12448  sumsplit  12479  binom  12536  bcxmas  12542  geomulcvg  12580  ruclem6  12761  smupf  12917  gcdcl  12944  pcxcl  13161  pcmptcl  13187  infpnlem2  13206  zgz  13228  4sqlem2  13244  4sqlem19  13258  vdwapval  13268  hashbc0  13300  ramcl2  13311  0ramcl  13318  ramcl  13324  isstruct2  13405  imasval  13664  imasbas  13665  imasds  13666  imasplusg  13670  imasmulr  13671  imasvsca  13673  imasle  13675  divsaddvallem  13703  divsaddflem  13704  divsaddval  13705  divsaddf  13706  divsmulval  13707  divsmulf  13708  mreexexlem3d  13798  sscpwex  13942  fullresc  13975  evlfcl  14246  ipopos  14513  submnd0  14652  gsumress  14704  divsgrp2  14863  issubg2  14886  torsubg  15396  frgpnabllem1  15411  lt6abl  15431  ablfaclem3  15572  ablfac2  15574  rngidss  15617  divsrng2  15653  isdrngd  15787  islss3  15962  lspsnel  16006  lspprel  16093  znf1o  16755  frgpcyg  16777  phlpropd  16809  cssval  16832  iscss  16833  indistopon  16988  indiscld  17078  restbas  17144  ordttopon  17179  iocpnfordt  17201  icomnfordt  17202  lecldbas  17205  fiuncmp  17389  cmpfi  17393  concompid  17415  elpt  17525  xkotop  17541  xkouni  17552  xkohaus  17606  xkoptsub  17607  imastopn  17673  filcon  17836  cfinufil  17881  alexsublem  17996  alexsub  17997  alexsubALTlem4  18002  distgp  18050  indistgp  18051  ssbl  18345  xmeter  18353  nmoi  18633  nmoeq0  18641  0nghm  18646  idnghm  18648  icccld  18672  iocmnfcld  18674  blssioo  18697  xrtgioo  18708  xrsxmet  18711  icccmp  18727  pcopt  18918  pcopt2  18919  elpi1  18941  cmetcaulem  19112  ishl2  19191  ovolcl  19241  ovolunlem1a  19259  ovolunnul  19263  ovoliunnul  19270  ioombl1  19323  icombl  19325  ioombl  19326  iccmbl  19327  iccvolcl  19328  ovolioo  19329  ioorcl  19336  uniioovol  19338  uniioombllem2a  19341  uniioombllem4  19345  uniioombllem5  19346  vitalilem1  19367  vitalilem5  19371  mbfconstlem  19388  mbfima  19391  mbfid  19395  ismbf2d  19400  mbfss  19405  mbfmulc2lem  19406  i1fd  19440  itg1addlem2  19456  itg1addlem4  19458  itg1addlem5  19459  i1fmulc  19462  itg2l  19488  itg2cl  19491  ibl0  19545  iblrelem  19549  iblpos  19551  iblss2  19564  bddmulibl  19597  recnperf  19659  ply1remlem  19952  fta1glem1  19955  fta1g  19957  elply  19981  plypf1  19998  coefv0  20033  coemulc  20040  fta1  20092  elqaalem2  20104  aannenlem2  20113  aalioulem3  20118  taylfvallem1  20140  tayl0  20145  ulm0  20174  logtayl  20418  atanrecl  20618  atanbnd  20633  harmonicbnd3  20713  ftalem7  20728  basellem5  20734  ppifi  20755  sqff1o  20832  1sgmprm  20850  logexprlim  20876  dchrelbasd  20890  dchr1re  20914  lgslem4  20950  lgsne0  20984  2sqlem9  21024  2sqlem10  21025  rpvmasumlem  21048  dchrisumlem1  21050  vmalogdivsum  21100  pntrlog2bndlem5  21142  ostth  21200  vdgrf  21517  eupath  21551  0blo  22141  nmlno0lem  22142  omlsilem  22752  pjoc1i  22781  nonbooli  23001  nmlnop0iALT  23346  unopbd  23366  leoprf2  23478  opsqrlem4  23494  opsqrlem5  23495  pjbdlni  23500  pjcmul1i  23552  esumcst  24251  dstfrvclim1  24514  ballotlemfelz  24527  subfacp1lem3  24647  rellyscon  24717  cvmlift2lem9  24777  prodrblem  25034  fprodcvg  25035  prodmolem2a  25039  zprod  25042  fprodntriv  25047  prodss  25052  fprodss  25053  bdayelon  25358  axlowdimlem16  25610  bpoly1  25811  bpoly2  25817  bpoly3  25818  ordcmp  25911  voliunnfl  25955  itg2addnclem2  25958  bddiblnc  25975  heiborlem4  26214  heiborlem6  26216  wepwsolem  26807  dsmm0cl  26875  uvcvvcl  26905  flcidc  27048  cnmsgnsubg  27103  lhe4.4ex1a  27215  dvconstbi  27220  climneg  27404  ioovolcl  27410  itgsinexplem1  27416  stoweidlem36  27453  wallispilem3  27484
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2380  df-clel 2383
  Copyright terms: Public domain W3C validator