Theorem syl6eqel 2531

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 2517	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1369   e. wcel 1756

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-cleq 2436  df-clel 2439

This theorem is referenced by:  syl6eqelr  2532  csbexg  4445  unisn2  4449  class2set  4480  snexALT  4499  snex  4554  prex  4555  onun2i  4855  iotaex  5419  fvrn0  5733  f0cli  5875  fmptsng  5921  elimdelov  6188  ndmovcl  6269  caovmo  6321  soex  6542  zfrep6  6566  1st2ndb  6635  smofvon2  6838  tz7.44-2  6884  oesuclem  6986  omcl  6997  oecl  6998  nnmcl  7072  nnecl  7073  ixpexg  7308  resixpfo  7322  en1b  7398  xpsnen  7416  nnunifi  7584  xpfi  7604  fsuppun  7660  0fsupp  7663  oiexg  7770  hartogslem1  7777  noinfepOLD  7887  cantnfvalf  7894  rankdmr1  8029  rankr1c  8049  numwdom  8250  alephon  8260  isfin5  8489  sdom2en01  8492  isf32lem9  8551  hsmexlem9  8615  iundom2g  8725  gchxpidm  8857  r1tskina  8970  tskmcl  9029  recmulnq  9154  recclnq  9156  genpelv  9190  un0mulcl  10635  znegcl  10701  zeo  10748  eqreznegel  10961  xnegcl  11204  ioorebas  11412  modid0  11754  modidmul0  11755  2txmodxeq0  11780  fzofi  11817  expcllem  11897  m1expcl2  11908  faclbnd4lem3  12092  bccl  12119  hasheq0  12152  hashrabrsn  12158  hashimarn  12221  cshwcl  12456  abs00bd  12801  iserge0  13159  sumrblem  13209  fsumcvg  13210  summolem2a  13213  sumss  13222  fsumss  13223  fsumcvg2  13225  sumsplit  13256  binom  13314  bcxmas  13319  geomulcvg  13357  ruclem6  13538  smupf  13695  gcdcl  13722  pcxcl  13948  pcmptcl  13974  infpnlem2  13993  zgz  14015  4sqlem2  14031  4sqlem19  14045  vdwapval  14055  hashbc0  14087  ramcl2  14098  0ramcl  14105  ramcl  14111  isstruct2  14204  imasval  14470  imasbas  14471  imasds  14472  imasplusg  14476  imasmulr  14477  imasvsca  14479  imasip  14480  imasle  14482  divsaddvallem  14510  divsaddflem  14511  divsaddval  14512  divsaddf  14513  divsmulval  14514  divsmulf  14515  mreexexlem3d  14605  sscpwex  14749  fullresc  14782  evlfcl  15053  ipopos  15351  submnd0  15472  gsumress  15528  divsgrp2  15694  issubg2  15717  torsubg  16357  frgpnabllem1  16372  lt6abl  16392  ablfaclem3  16610  ablfac2  16612  srgbinomlem3  16662  rngidss  16693  divsrng2  16734  isdrngd  16879  mptscmfsupp0  17033  islss3  17062  lspsnel  17106  lspprel  17197  znf1o  18006  frgpcyg  18028  cnmsgnsubg  18029  phlpropd  18106  cssval  18129  iscss  18130  dsmm0cl  18187  uvcvvcl  18234  m2detleiblem1  18452  indistopon  18627  indiscld  18717  restbas  18784  ordttopon  18819  iocpnfordt  18841  icomnfordt  18842  lecldbas  18845  fiuncmp  19029  cmpfi  19033  concompid  19057  elpt  19167  xkotop  19183  xkouni  19194  xkohaus  19248  xkoptsub  19249  imastopn  19315  filcon  19478  cfinufil  19523  alexsublem  19638  alexsub  19639  alexsubALTlem4  19644  distgp  19692  indistgp  19693  ssblps  20019  ssbl  20020  xmeter  20030  nmoi  20329  nmoeq0  20337  0nghm  20342  idnghm  20344  icccld  20368  iocmnfcld  20370  blssioo  20394  xrtgioo  20405  xrsxmet  20408  icccmp  20424  pcopt  20616  pcopt2  20617  elpi1  20639  cmetcaulem  20821  ishl2  20904  rrxmvallem  20925  ovolcl  20983  ovolunlem1a  21001  ovolunnul  21005  ovoliunnul  21012  ioombl1  21065  icombl  21067  ioombl  21068  iccmbl  21069  iccvolcl  21070  ovolioo  21071  ioovolcl  21072  ioorcl  21079  uniioovol  21081  uniioombllem2a  21084  uniioombllem4  21088  uniioombllem5  21089  vitalilem1  21110  vitalilem5  21114  mbfconstlem  21129  mbfima  21132  mbfid  21136  ismbf2d  21141  mbfss  21146  mbfmulc2lem  21147  i1fd  21181  itg1addlem2  21197  itg1addlem4  21199  itg1addlem5  21200  i1fmulc  21203  itg2l  21229  itg2cl  21232  ibl0  21286  iblrelem  21290  iblpos  21292  iblss2  21305  bddmulibl  21338  recnperf  21402  ply1remlem  21656  fta1glem1  21659  fta1g  21661  elply  21685  plypf1  21702  coefv0  21737  coemulc  21744  fta1  21796  elqaalem2  21808  aannenlem2  21817  aalioulem3  21822  taylfvallem1  21844  tayl0  21849  ulm0  21878  logtayl  22127  atanrecl  22328  atanbnd  22343  harmonicbnd3  22423  ftalem7  22438  basellem5  22444  ppifi  22465  sqff1o  22542  1sgmprm  22560  logexprlim  22586  dchrelbasd  22600  dchr1re  22624  lgslem4  22660  lgsne0  22694  2sqlem9  22734  2sqlem10  22735  rpvmasumlem  22758  dchrisumlem1  22760  vmalogdivsum  22810  pntrlog2bndlem5  22852  ostth  22910  axlowdimlem16  23225  vdgrf  23590  eupath  23624  0blo  24214  nmlno0lem  24215  omlsilem  24827  pjoc1i  24856  nonbooli  25076  nmlnop0iALT  25421  unopbd  25441  leoprf2  25553  opsqrlem4  25569  opsqrlem5  25570  pjbdlni  25575  pjcmul1i  25627  sgnsf  26214  prsssdm  26369  ordtrestNEW  26373  esumcst  26536  sibf0  26742  sitgclcn  26752  sitgclre  26753  eulerpartlemgs2  26785  dstfrvclim1  26882  ballotlemfelz  26895  sgncl  26943  signstfveq0  27000  subfacp1lem3  27092  rellyscon  27162  cvmlift2lem9  27222  prodrblem  27464  fprodcvg  27465  prodmolem2a  27469  zprod  27472  fprodntriv  27477  prodss  27482  fprodss  27483  binomfallfac  27566  bdayelon  27843  bpoly1  28216  bpoly2  28222  bpoly3  28223  ordcmp  28315  voliunnfl  28461  mbfresfi  28464  itg2addnclem2  28470  bddiblnc  28488  dvasin  28506  heiborlem4  28739  heiborlem6  28741  wepwsolem  29420  flcidc  29557  iocmbl  29614  arearect  29617  lhe4.4ex1a  29629  dvconstbi  29634  climneg  29809  itgsinexplem1  29820  stoweidlem36  29857  wallispilem3  29888  fmptsnd  30748  m1detdiag  30931  lincext2  30986