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

Theorem syl6eqel 2384
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 10 . 2  |-  ( ph  ->  B  e.  C )
41, 3eqeltrd 2370 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    e. wcel 1696
This theorem is referenced by:  syl6eqelr  2385  class2set  4194  snexALT  4212  snex  4232  prex  4233  onun2i  4524  unisn2  4538  soex  5138  iotaex  5252  fvrn0  5566  f0cli  5687  zfrep6  5764  elimdelov  5943  ndmovcl  6021  caovmo  6073  1st2ndb  6176  smofvon2  6389  tz7.44-2  6436  oesuclem  6540  omcl  6551  oecl  6552  nnmcl  6626  nnecl  6627  ixpexg  6856  resixpfo  6870  en1b  6945  xpsnen  6962  nnunifi  7124  xpfi  7144  oiexg  7266  hartogslem1  7273  noinfepOLD  7377  cantnfvalf  7382  cantnf0  7392  rankdmr1  7489  rankr1c  7509  numwdom  7702  alephon  7712  isfin5  7941  sdom2en01  7944  isf32lem9  8003  hsmexlem9  8067  iundom2g  8178  gchxpidm  8307  r1tskina  8420  tskmcl  8479  recmulnq  8604  recclnq  8606  genpelv  8640  un0mulcl  10014  znegcl  10071  zeo  10113  eqreznegel  10319  xnegcl  10556  ioorebas  10761  fzofi  11052  expcllem  11130  m1expcl2  11141  faclbnd4lem3  11324  bccl  11350  hasheq0  11369  abs00bd  11792  iserge0  12150  sumrblem  12200  fsumcvg  12201  summolem2a  12204  zsum  12207  sumss  12213  fsumss  12214  fsumcvg2  12216  sumsplit  12247  binom  12304  bcxmas  12310  geomulcvg  12348  ruclem6  12529  smupf  12685  gcdcl  12712  pcxcl  12929  pcmptcl  12955  infpnlem2  12974  zgz  12996  4sqlem2  13012  4sqlem19  13026  vdwapval  13036  hashbc0  13068  ramcl2  13079  0ramcl  13086  ramcl  13092  isstruct2  13173  imasval  13430  imasbas  13431  imasds  13432  imasplusg  13436  imasmulr  13437  imasvsca  13439  imasle  13441  divsaddvallem  13469  divsaddflem  13470  divsaddval  13471  divsaddf  13472  divsmulval  13473  divsmulf  13474  mreexexlem3d  13564  sscpwex  13708  fullresc  13741  evlfcl  14012  ipopos  14279  submnd0  14418  gsumress  14470  divsgrp2  14629  issubg2  14652  torsubg  15162  frgpnabllem1  15177  lt6abl  15197  ablfaclem3  15338  ablfac2  15340  rngidss  15383  divsrng2  15419  isdrngd  15553  islss3  15732  lspsnel  15776  lspprel  15863  znf1o  16521  frgpcyg  16543  phlpropd  16575  cssval  16598  iscss  16599  indistopon  16754  indiscld  16844  restbas  16905  ordttopon  16939  iocpnfordt  16961  icomnfordt  16962  lecldbas  16965  fiuncmp  17147  cmpfi  17151  concompid  17173  elpt  17283  xkotop  17299  xkouni  17310  xkohaus  17363  xkoptsub  17364  imastopn  17427  filcon  17594  cfinufil  17639  alexsublem  17754  alexsub  17755  alexsubALTlem4  17760  distgp  17798  indistgp  17799  imasdsf1olem  17953  imasf1oxmet  17955  ssbl  17987  xmeter  17995  nmoi  18253  nmoeq0  18261  0nghm  18266  idnghm  18268  icccld  18292  iocmnfcld  18294  blssioo  18317  xrtgioo  18328  xrsxmet  18331  icccmp  18346  pcopt  18536  pcopt2  18537  elpi1  18559  cmetcaulem  18730  ishl2  18803  ovolcl  18853  ovolunlem1a  18871  ovolunnul  18875  ovoliunnul  18882  ioombl1  18935  icombl  18937  ioombl  18938  iccmbl  18939  iccvolcl  18940  ovolioo  18941  ioorcl  18948  uniioovol  18950  uniioombllem2a  18953  uniioombllem4  18957  uniioombllem5  18958  vitalilem1  18979  vitalilem5  18983  mbfconstlem  19000  mbfima  19003  mbfid  19007  ismbf2d  19012  mbfss  19017  mbfmulc2lem  19018  i1fd  19052  itg1addlem2  19068  itg1addlem4  19070  itg1addlem5  19071  i1fmulc  19074  itg2l  19100  itg2cl  19103  ibl0  19157  iblrelem  19161  iblpos  19163  iblss2  19176  bddmulibl  19209  recnperf  19271  ply1remlem  19564  fta1glem1  19567  fta1g  19569  elply  19593  plypf1  19610  coefv0  19645  coemulc  19652  fta1  19704  elqaalem2  19716  aannenlem2  19725  aalioulem3  19730  taylfvallem1  19752  tayl0  19757  ulm0  19786  logtayl  20023  atanrecl  20223  atanbnd  20238  harmonicbnd3  20317  ftalem7  20332  basellem5  20338  ppifi  20359  sqff1o  20436  1sgmprm  20454  logexprlim  20480  dchrelbasd  20494  dchr1re  20518  lgslem4  20554  lgsne0  20588  2sqlem9  20628  2sqlem10  20629  rpvmasumlem  20652  dchrisumlem1  20654  vmalogdivsum  20704  pntrlog2bndlem5  20746  ostth  20804  0blo  21386  nmlno0lem  21387  omlsilem  21997  pjoc1i  22026  nonbooli  22246  nmlnop0iALT  22591  unopbd  22611  leoprf2  22723  opsqrlem4  22739  opsqrlem5  22740  pjbdlni  22745  pjcmul1i  22797  esumcst  23451  subfacp1lem3  23728  rellyscon  23797  cvmlift2lem9  23857  eupath  23920  prodrblem  24152  fprodcvg  24153  prodmolem2a  24157  zprod  24160  bdayelon  24405  axlowdimlem16  24657  bpoly1  24858  bpoly2  24864  bpoly3  24865  ordcmp  24958  itg2addnclem2  25004  bddiblnc  25021  stcat  25147  eloi  25189  fixpc  25197  intvconlem1  25806  aidm2  25853  vtarsuelt  25998  isside0  26267  heiborlem4  26641  heiborlem6  26643  wepwsolem  27241  dsmm0cl  27309  uvcvvcl  27339  flcidc  27482  cnmsgnsubg  27537  lhe4.4ex1a  27649  dvconstbi  27654  ioovolcl  27845  stoweidlem36  27888
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