Theorem syl6eqel 2498

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

Step	Hyp	Ref	Expression
1		syl6eqel.1	. 2 |- ( ph -> A = B )
2		syl6eqel.2	. . 3 |- B e. C
3	2	a1i 11	. 2 |- ( ph -> B e. C )
4	1, 3	eqeltrd 2490	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1405   e. wcel 1842

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1634  df-cleq 2394  df-clel 2397

This theorem is referenced by:  syl6eqelr  2499  csbexg  4527  unisn2  4529  class2set  4560  snexALT  4579  snex  4631  prex  4632  onun2i  5524  iotaex  5549  fvrn0  5870  f0cli  6019  fmptsng  6071  fmptsnd  6072  elimdelov  6358  ovima0  6434  ndmovcl  6440  caovmo  6492  soex  6726  zfrep6  6751  1st2ndb  6821  wfrlem17  7036  smofvon2  7059  tz7.44-2  7109  oesuclem  7211  omcl  7222  oecl  7223  nnmcl  7297  nnecl  7298  ixpexg  7530  resixpfo  7544  en1b  7620  xpsnen  7638  nnunifi  7804  xpfi  7824  fsuppun  7881  0fsupp  7884  oiexg  7993  hartogslem1  8000  cantnfvalf  8115  rankdmr1  8250  rankr1c  8270  numwdom  8471  alephon  8481  isfin5  8710  sdom2en01  8713  isf32lem9  8772  hsmexlem9  8836  iundom2g  8946  gchxpidm  9076  r1tskina  9189  tskmcl  9248  recmulnq  9371  recclnq  9373  genpelv  9407  un0mulcl  10870  znegcl  10939  zeo  10988  eqreznegel  11211  xnegcl  11464  ioorebas  11678  modid0  12058  modidmul0OLD  12059  2txmodxeq0  12086  fzofi  12123  expcllem  12219  m1expcl2  12230  faclbnd4lem3  12415  bccl  12442  hasheq0  12479  hashrabrsn  12486  hashimarn  12543  ccat2s1p1  12684  cshwcl  12823  relexpaddg  13033  abs00bd  13271  iserge0  13630  sumrblem  13680  fsumcvg  13681  summolem2a  13684  sumss  13693  fsumss  13694  fsumcvg2  13696  sumsplit  13732  binom  13791  bcxmas  13796  geomulcvg  13835  prodrblem  13886  fprodcvg  13887  prodmolem2a  13891  zprod  13894  fprodntriv  13899  prodss  13904  fprodss  13905  binomfallfac  13984  bpoly1  13994  bpoly2  14000  bpoly3  14001  ruclem6  14175  smupf  14335  gcdcl  14362  pcxcl  14591  pcmptcl  14617  infpnlem2  14636  zgz  14658  4sqlem2  14674  4sqlem19  14688  vdwapval  14698  hashbc0  14730  ramcl2  14741  0ramcl  14748  ramcl  14754  isstruct2  14848  imasval  15123  imasbas  15124  imasds  15125  imasplusg  15129  imasmulr  15130  imasvsca  15132  imasip  15133  imasle  15135  qusaddvallem  15163  qusaddflem  15164  qusaddval  15165  qusaddf  15166  qusmulval  15167  qusmulf  15168  mreexexlem3d  15258  sscpwex  15426  fullresc  15462  estrres  15730  evlfcl  15813  ipopos  16112  gsumress  16225  submnd0  16272  qusgrp2  16510  issubg2  16538  torsubg  17182  frgpnabllem1  17199  lt6abl  17219  ablfaclem3  17456  ablfac2  17458  srgbinomlem3  17511  ringidss  17543  qusring2  17587  isdrngd  17739  mptscmfsupp0  17894  islss3  17923  lspsnel  17967  lspprel  18058  znf1o  18886  frgpcyg  18908  cnmsgnsubg  18909  phlpropd  18986  cssval  19009  iscss  19010  dsmm0cl  19067  uvcvvcl  19112  m1detdiag  19389  m2detleiblem1  19416  pmatcollpw3fi1lem1  19577  indistopon  19792  indiscld  19883  restbas  19950  ordttopon  19985  iocpnfordt  20007  icomnfordt  20008  lecldbas  20011  fiuncmp  20195  cmpfi  20199  concompid  20222  dissnlocfin  20320  elpt  20363  xkotop  20379  xkouni  20390  xkohaus  20444  xkoptsub  20445  imastopn  20511  filcon  20674  cfinufil  20719  alexsublem  20834  alexsub  20835  alexsubALTlem4  20840  distgp  20888  indistgp  20889  ssblps  21215  ssbl  21216  xmeter  21226  nmoi  21525  nmoeq0  21533  0nghm  21538  idnghm  21540  icccld  21564  iocmnfcld  21566  blssioo  21590  xrtgioo  21601  xrsxmet  21604  icccmp  21620  pcopt  21812  pcopt2  21813  elpi1  21835  cmetcaulem  22017  ishl2  22100  rrxmvallem  22121  ovolcl  22179  ovolunlem1a  22197  ovolunnul  22201  ovoliunnul  22208  ioombl1  22262  icombl  22264  ioombl  22265  iccmbl  22266  iccvolcl  22267  ovolioo  22268  ioovolcl  22269  ioorcl  22276  uniioovol  22278  uniioombllem2a  22281  uniioombllem4  22285  uniioombllem5  22286  vitalilem1  22307  vitalilem5  22311  mbfconstlem  22326  mbfima  22329  mbfid  22333  ismbf2d  22338  mbfss  22343  mbfmulc2lem  22344  i1fd  22378  itg1addlem2  22394  itg1addlem4  22396  itg1addlem5  22397  i1fmulc  22400  itg2l  22426  itg2cl  22429  ibl0  22483  iblrelem  22487  iblpos  22489  iblss2  22502  bddmulibl  22535  recnperf  22599  ply1remlem  22853  fta1glem1  22856  fta1g  22858  elply  22882  plypf1  22899  coefv0  22935  coemulc  22942  fta1  22994  elqaalem2  23006  aannenlem2  23015  aalioulem3  23020  taylfvallem1  23042  tayl0  23047  ulm0  23076  logtayl  23333  atanrecl  23565  atanbnd  23580  harmonicbnd3  23661  ftalem7  23731  basellem5  23737  ppifi  23758  sqff1o  23835  1sgmprm  23853  logexprlim  23879  dchrelbasd  23893  dchr1re  23917  lgslem4  23953  lgsne0  23987  2sqlem9  24027  2sqlem10  24028  rpvmasumlem  24051  dchrisumlem1  24053  vmalogdivsum  24103  pntrlog2bndlem5  24145  ostth  24203  axlowdimlem16  24664  vdgrf  25302  eupath  25385  0blo  26107  nmlno0lem  26108  omlsilem  26720  pjoc1i  26749  nonbooli  26969  nmlnop0iALT  27313  unopbd  27333  leoprf2  27445  opsqrlem4  27461  opsqrlem5  27462  pjbdlni  27467  pjcmul1i  27519  prsssdm  28338  ordtrestNEW  28342  esumpad  28488  esumpad2  28489  esumcst  28496  esumrnmpt2  28501  sibf0  28768  sitgclcn  28778  sitgclre  28779  eulerpartlemgs2  28811  dstfrvclim1  28908  ballotlemfelz  28921  sgncl  28969  signstfveq0  29026  subfacp1lem3  29466  rellyscon  29535  cvmlift2lem9  29595  bdayelon  30127  ordcmp  30666  voliunnfl  31410  mbfresfi  31413  itg2addnclem2  31420  bddiblnc  31438  dvasin  31454  heiborlem4  31572  heiborlem6  31574  wepwsolem  35329  flcidc  35467  iocmbl  35524  arearect  35527  briunov2uz  35657  eliunov2uz  35658  frege124d  35720  frege129d  35722  frege92  35916  lcmcl  36035  lhe4.4ex1a  36062  dvconstbi  36067  binomcxplemnn0  36082  binomcxplemnotnn0  36089  climneg  36965  cncfiooicc  37046  itgsinexplem1  37101  stoweidlem36  37167  wallispilem3  37198  fourierdlem93  37331  fouriersw  37363  fouriercn  37364  etransclem16  37382  etransclem33  37399  nnsum4primeseven  37829  nnsum4primesevenALTV  37830  lincext2  38548  blennn0elnn  38689