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

Theorem syl6eqel 2371
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 2357 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684
This theorem is referenced by:  syl6eqelr  2372  class2set  4178  snexALT  4196  snex  4216  prex  4217  onun2i  4508  unisn2  4522  soex  5122  iotaex  5236  fvrn0  5550  f0cli  5671  zfrep6  5748  elimdelov  5927  ndmovcl  6005  caovmo  6057  1st2ndb  6160  smofvon2  6373  tz7.44-2  6420  oesuclem  6524  omcl  6535  oecl  6536  nnmcl  6610  nnecl  6611  ixpexg  6840  resixpfo  6854  en1b  6929  xpsnen  6946  nnunifi  7108  xpfi  7128  oiexg  7250  hartogslem1  7257  noinfepOLD  7361  cantnfvalf  7366  cantnf0  7376  rankdmr1  7473  rankr1c  7493  numwdom  7686  alephon  7696  isfin5  7925  sdom2en01  7928  isf32lem9  7987  hsmexlem9  8051  iundom2g  8162  gchxpidm  8291  r1tskina  8404  tskmcl  8463  recmulnq  8588  recclnq  8590  genpelv  8624  un0mulcl  9998  znegcl  10055  zeo  10097  eqreznegel  10303  xnegcl  10540  ioorebas  10745  fzofi  11036  expcllem  11114  m1expcl2  11125  faclbnd4lem3  11308  bccl  11334  hasheq0  11353  abs00bd  11776  iserge0  12134  sumrblem  12184  fsumcvg  12185  summolem2a  12188  zsum  12191  sumss  12197  fsumss  12198  fsumcvg2  12200  sumsplit  12231  binom  12288  bcxmas  12294  geomulcvg  12332  ruclem6  12513  smupf  12669  gcdcl  12696  pcxcl  12913  pcmptcl  12939  infpnlem2  12958  zgz  12980  4sqlem2  12996  4sqlem19  13010  vdwapval  13020  hashbc0  13052  ramcl2  13063  0ramcl  13070  ramcl  13076  isstruct2  13157  imasval  13414  imasbas  13415  imasds  13416  imasplusg  13420  imasmulr  13421  imasvsca  13423  imasle  13425  divsaddvallem  13453  divsaddflem  13454  divsaddval  13455  divsaddf  13456  divsmulval  13457  divsmulf  13458  mreexexlem3d  13548  sscpwex  13692  fullresc  13725  evlfcl  13996  ipopos  14263  submnd0  14402  gsumress  14454  divsgrp2  14613  issubg2  14636  torsubg  15146  frgpnabllem1  15161  lt6abl  15181  ablfaclem3  15322  ablfac2  15324  rngidss  15367  divsrng2  15403  isdrngd  15537  islss3  15716  lspsnel  15760  lspprel  15847  znf1o  16505  frgpcyg  16527  phlpropd  16559  cssval  16582  iscss  16583  indistopon  16738  indiscld  16828  restbas  16889  ordttopon  16923  iocpnfordt  16945  icomnfordt  16946  lecldbas  16949  fiuncmp  17131  cmpfi  17135  concompid  17157  elpt  17267  xkotop  17283  xkouni  17294  xkohaus  17347  xkoptsub  17348  imastopn  17411  filcon  17578  cfinufil  17623  alexsublem  17738  alexsub  17739  alexsubALTlem4  17744  distgp  17782  indistgp  17783  imasdsf1olem  17937  imasf1oxmet  17939  ssbl  17971  xmeter  17979  nmoi  18237  nmoeq0  18245  0nghm  18250  idnghm  18252  icccld  18276  iocmnfcld  18278  blssioo  18301  xrtgioo  18312  xrsxmet  18315  icccmp  18330  pcopt  18520  pcopt2  18521  elpi1  18543  cmetcaulem  18714  ishl2  18787  ovolcl  18837  ovolunlem1a  18855  ovolunnul  18859  ovoliunnul  18866  ioombl1  18919  icombl  18921  ioombl  18922  iccmbl  18923  iccvolcl  18924  ovolioo  18925  ioorcl  18932  uniioovol  18934  uniioombllem2a  18937  uniioombllem4  18941  uniioombllem5  18942  vitalilem1  18963  vitalilem5  18967  mbfconstlem  18984  mbfima  18987  mbfid  18991  ismbf2d  18996  mbfss  19001  mbfmulc2lem  19002  i1fd  19036  itg1addlem2  19052  itg1addlem4  19054  itg1addlem5  19055  i1fmulc  19058  itg2l  19084  itg2cl  19087  ibl0  19141  iblrelem  19145  iblpos  19147  iblss2  19160  bddmulibl  19193  recnperf  19255  ply1remlem  19548  fta1glem1  19551  fta1g  19553  elply  19577  plypf1  19594  coefv0  19629  coemulc  19636  fta1  19688  elqaalem2  19700  aannenlem2  19709  aalioulem3  19714  taylfvallem1  19736  tayl0  19741  ulm0  19770  logtayl  20007  atanrecl  20207  atanbnd  20222  harmonicbnd3  20301  ftalem7  20316  basellem5  20322  ppifi  20343  sqff1o  20420  1sgmprm  20438  logexprlim  20464  dchrelbasd  20478  dchr1re  20502  lgslem4  20538  lgsne0  20572  2sqlem9  20612  2sqlem10  20613  rpvmasumlem  20636  dchrisumlem1  20638  vmalogdivsum  20688  pntrlog2bndlem5  20730  ostth  20788  0blo  21370  nmlno0lem  21371  omlsilem  21981  pjoc1i  22010  nonbooli  22230  nmlnop0iALT  22575  unopbd  22595  leoprf2  22707  opsqrlem4  22723  opsqrlem5  22724  pjbdlni  22729  pjcmul1i  22781  esumcst  23436  subfacp1lem3  23713  rellyscon  23782  cvmlift2lem9  23842  eupath  23905  bdayelon  24334  axlowdimlem16  24585  bpoly1  24786  bpoly2  24792  bpoly3  24793  ordcmp  24886  stcat  25044  eloi  25086  fixpc  25094  intvconlem1  25703  aidm2  25750  vtarsuelt  25895  isside0  26164  heiborlem4  26538  heiborlem6  26540  wepwsolem  27138  dsmm0cl  27206  uvcvvcl  27236  flcidc  27379  cnmsgnsubg  27434  lhe4.4ex1a  27546  dvconstbi  27551  ioovolcl  27742  stoweidlem36  27785
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