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

Theorem syl6eqel 2523
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 2509 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    e. wcel 1725
This theorem is referenced by:  syl6eqelr  2524  class2set  4359  snexALT  4377  snex  4397  prex  4398  onun2i  4689  unisn2  4703  soex  5311  iotaex  5427  fvrn0  5745  f0cli  5872  zfrep6  5960  elimdelov  6145  ndmovcl  6224  caovmo  6276  1st2ndb  6379  smofvon2  6610  tz7.44-2  6657  oesuclem  6761  omcl  6772  oecl  6773  nnmcl  6847  nnecl  6848  ixpexg  7078  resixpfo  7092  en1b  7167  xpsnen  7184  nnunifi  7350  xpfi  7370  oiexg  7496  hartogslem1  7503  noinfepOLD  7607  cantnfvalf  7612  cantnf0  7622  rankdmr1  7719  rankr1c  7739  numwdom  7932  alephon  7942  isfin5  8171  sdom2en01  8174  isf32lem9  8233  hsmexlem9  8297  iundom2g  8407  gchxpidm  8536  r1tskina  8649  tskmcl  8708  recmulnq  8833  recclnq  8835  genpelv  8869  un0mulcl  10246  znegcl  10305  zeo  10347  eqreznegel  10553  xnegcl  10791  ioorebas  10998  fzofi  11305  expcllem  11384  m1expcl2  11395  faclbnd4lem3  11578  bccl  11605  hasheq0  11636  hashrabrsn  11640  abs00bd  12088  iserge0  12446  sumrblem  12497  fsumcvg  12498  summolem2a  12501  zsum  12504  sumss  12510  fsumss  12511  fsumcvg2  12513  sumsplit  12544  binom  12601  bcxmas  12607  geomulcvg  12645  ruclem6  12826  smupf  12982  gcdcl  13009  pcxcl  13226  pcmptcl  13252  infpnlem2  13271  zgz  13293  4sqlem2  13309  4sqlem19  13323  vdwapval  13333  hashbc0  13365  ramcl2  13376  0ramcl  13383  ramcl  13389  isstruct2  13470  imasval  13729  imasbas  13730  imasds  13731  imasplusg  13735  imasmulr  13736  imasvsca  13738  imasle  13740  divsaddvallem  13768  divsaddflem  13769  divsaddval  13770  divsaddf  13771  divsmulval  13772  divsmulf  13773  mreexexlem3d  13863  sscpwex  14007  fullresc  14040  evlfcl  14311  ipopos  14578  submnd0  14717  gsumress  14769  divsgrp2  14928  issubg2  14951  torsubg  15461  frgpnabllem1  15476  lt6abl  15496  ablfaclem3  15637  ablfac2  15639  rngidss  15682  divsrng2  15718  isdrngd  15852  islss3  16027  lspsnel  16071  lspprel  16158  znf1o  16824  frgpcyg  16846  phlpropd  16878  cssval  16901  iscss  16902  indistopon  17057  indiscld  17147  restbas  17214  ordttopon  17249  iocpnfordt  17271  icomnfordt  17272  lecldbas  17275  fiuncmp  17459  cmpfi  17463  concompid  17486  elpt  17596  xkotop  17612  xkouni  17623  xkohaus  17677  xkoptsub  17678  imastopn  17744  filcon  17907  cfinufil  17952  alexsublem  18067  alexsub  18068  alexsubALTlem4  18073  distgp  18121  indistgp  18122  ssblps  18444  ssbl  18445  xmeter  18455  nmoi  18754  nmoeq0  18762  0nghm  18767  idnghm  18769  icccld  18793  iocmnfcld  18795  blssioo  18818  xrtgioo  18829  xrsxmet  18832  icccmp  18848  pcopt  19039  pcopt2  19040  elpi1  19062  cmetcaulem  19233  ishl2  19316  ovolcl  19366  ovolunlem1a  19384  ovolunnul  19388  ovoliunnul  19395  ioombl1  19448  icombl  19450  ioombl  19451  iccmbl  19452  iccvolcl  19453  ovolioo  19454  ioorcl  19461  uniioovol  19463  uniioombllem2a  19466  uniioombllem4  19470  uniioombllem5  19471  vitalilem1  19492  vitalilem5  19496  mbfconstlem  19513  mbfima  19516  mbfid  19520  ismbf2d  19525  mbfss  19530  mbfmulc2lem  19531  i1fd  19565  itg1addlem2  19581  itg1addlem4  19583  itg1addlem5  19584  i1fmulc  19587  itg2l  19613  itg2cl  19616  ibl0  19670  iblrelem  19674  iblpos  19676  iblss2  19689  bddmulibl  19722  recnperf  19784  ply1remlem  20077  fta1glem1  20080  fta1g  20082  elply  20106  plypf1  20123  coefv0  20158  coemulc  20165  fta1  20217  elqaalem2  20229  aannenlem2  20238  aalioulem3  20243  taylfvallem1  20265  tayl0  20270  ulm0  20299  logtayl  20543  atanrecl  20743  atanbnd  20758  harmonicbnd3  20838  ftalem7  20853  basellem5  20859  ppifi  20880  sqff1o  20957  1sgmprm  20975  logexprlim  21001  dchrelbasd  21015  dchr1re  21039  lgslem4  21075  lgsne0  21109  2sqlem9  21149  2sqlem10  21150  rpvmasumlem  21173  dchrisumlem1  21175  vmalogdivsum  21225  pntrlog2bndlem5  21267  ostth  21325  vdgrf  21661  eupath  21695  0blo  22285  nmlno0lem  22286  omlsilem  22896  pjoc1i  22925  nonbooli  23145  nmlnop0iALT  23490  unopbd  23510  leoprf2  23622  opsqrlem4  23638  opsqrlem5  23639  pjbdlni  23644  pjcmul1i  23696  esumcst  24447  sibf0  24641  sitgclcn  24650  sitgclre  24651  dstfrvclim1  24727  ballotlemfelz  24740  subfacp1lem3  24860  rellyscon  24930  cvmlift2lem9  24990  prodrblem  25247  fprodcvg  25248  prodmolem2a  25252  zprod  25255  fprodntriv  25260  prodss  25265  fprodss  25266  binomfallfac  25349  bdayelon  25627  axlowdimlem16  25888  bpoly1  26089  bpoly2  26095  bpoly3  26096  ordcmp  26189  voliunnfl  26240  mbfresfi  26243  itg2addnclem2  26247  bddiblnc  26265  heiborlem4  26504  heiborlem6  26506  wepwsolem  27097  dsmm0cl  27164  uvcvvcl  27194  flcidc  27337  cnmsgnsubg  27392  lhe4.4ex1a  27504  dvconstbi  27509  climneg  27693  ioovolcl  27699  itgsinexplem1  27705  stoweidlem36  27742  wallispilem3  27773  modid0  28127  modidmul0  28128  2txmodxeq0  28130  hashimarn  28131  cshwcl  28196
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 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-cleq 2428  df-clel 2431
  Copyright terms: Public domain W3C validator