Theorem syl6eqel 2563

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

Syntax hints:   -> wi 4   = wceq 1379   e. wcel 1767

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-cleq 2459  df-clel 2462

This theorem is referenced by:  syl6eqelr  2564  csbexg  4579  unisn2  4583  class2set  4614  snexALT  4633  snex  4688  prex  4689  onun2i  4993  iotaex  5568  fvrn0  5888  f0cli  6032  fmptsng  6082  fmptsnd  6083  elimdelov  6362  ndmovcl  6444  caovmo  6496  soex  6727  zfrep6  6752  1st2ndb  6822  smofvon2  7027  tz7.44-2  7073  oesuclem  7175  omcl  7186  oecl  7187  nnmcl  7261  nnecl  7262  ixpexg  7493  resixpfo  7507  en1b  7583  xpsnen  7601  nnunifi  7771  xpfi  7791  fsuppun  7848  0fsupp  7851  oiexg  7960  hartogslem1  7967  noinfepOLD  8077  cantnfvalf  8084  rankdmr1  8219  rankr1c  8239  numwdom  8440  alephon  8450  isfin5  8679  sdom2en01  8682  isf32lem9  8741  hsmexlem9  8805  iundom2g  8915  gchxpidm  9047  r1tskina  9160  tskmcl  9219  recmulnq  9342  recclnq  9344  genpelv  9378  un0mulcl  10830  znegcl  10898  zeo  10946  eqreznegel  11167  xnegcl  11412  ioorebas  11626  modid0  11989  modidmul0  11990  2txmodxeq0  12015  fzofi  12052  expcllem  12145  m1expcl2  12156  faclbnd4lem3  12341  bccl  12368  hasheq0  12401  hashrabrsn  12408  hashimarn  12462  cshwcl  12732  abs00bd  13087  iserge0  13446  sumrblem  13496  fsumcvg  13497  summolem2a  13500  sumss  13509  fsumss  13510  fsumcvg2  13512  sumsplit  13546  binom  13605  bcxmas  13610  geomulcvg  13648  ruclem6  13829  smupf  13987  gcdcl  14014  pcxcl  14243  pcmptcl  14269  infpnlem2  14288  zgz  14310  4sqlem2  14326  4sqlem19  14340  vdwapval  14350  hashbc0  14382  ramcl2  14393  0ramcl  14400  ramcl  14406  isstruct2  14499  imasval  14766  imasbas  14767  imasds  14768  imasplusg  14772  imasmulr  14773  imasvsca  14775  imasip  14776  imasle  14778  divsaddvallem  14806  divsaddflem  14807  divsaddval  14808  divsaddf  14809  divsmulval  14810  divsmulf  14811  mreexexlem3d  14901  sscpwex  15045  fullresc  15078  evlfcl  15349  ipopos  15647  submnd0  15769  gsumress  15829  divsgrp2  15998  issubg2  16021  torsubg  16663  frgpnabllem1  16680  lt6abl  16700  ablfaclem3  16940  ablfac2  16942  srgbinomlem3  16995  rngidss  17026  divsrng2  17070  isdrngd  17221  mptscmfsupp0  17376  islss3  17405  lspsnel  17449  lspprel  17540  znf1o  18385  frgpcyg  18407  cnmsgnsubg  18408  phlpropd  18485  cssval  18508  iscss  18509  dsmm0cl  18566  uvcvvcl  18613  m1detdiag  18894  m2detleiblem1  18921  pmatcollpw3fi1lem1  19082  indistopon  19296  indiscld  19386  restbas  19453  ordttopon  19488  iocpnfordt  19510  icomnfordt  19511  lecldbas  19514  fiuncmp  19698  cmpfi  19702  concompid  19726  elpt  19836  xkotop  19852  xkouni  19863  xkohaus  19917  xkoptsub  19918  imastopn  19984  filcon  20147  cfinufil  20192  alexsublem  20307  alexsub  20308  alexsubALTlem4  20313  distgp  20361  indistgp  20362  ssblps  20688  ssbl  20689  xmeter  20699  nmoi  20998  nmoeq0  21006  0nghm  21011  idnghm  21013  icccld  21037  iocmnfcld  21039  blssioo  21063  xrtgioo  21074  xrsxmet  21077  icccmp  21093  pcopt  21285  pcopt2  21286  elpi1  21308  cmetcaulem  21490  ishl2  21573  rrxmvallem  21594  ovolcl  21652  ovolunlem1a  21670  ovolunnul  21674  ovoliunnul  21681  ioombl1  21735  icombl  21737  ioombl  21738  iccmbl  21739  iccvolcl  21740  ovolioo  21741  ioovolcl  21742  ioorcl  21749  uniioovol  21751  uniioombllem2a  21754  uniioombllem4  21758  uniioombllem5  21759  vitalilem1  21780  vitalilem5  21784  mbfconstlem  21799  mbfima  21802  mbfid  21806  ismbf2d  21811  mbfss  21816  mbfmulc2lem  21817  i1fd  21851  itg1addlem2  21867  itg1addlem4  21869  itg1addlem5  21870  i1fmulc  21873  itg2l  21899  itg2cl  21902  ibl0  21956  iblrelem  21960  iblpos  21962  iblss2  21975  bddmulibl  22008  recnperf  22072  ply1remlem  22326  fta1glem1  22329  fta1g  22331  elply  22355  plypf1  22372  coefv0  22407  coemulc  22414  fta1  22466  elqaalem2  22478  aannenlem2  22487  aalioulem3  22492  taylfvallem1  22514  tayl0  22519  ulm0  22548  logtayl  22797  atanrecl  22998  atanbnd  23013  harmonicbnd3  23093  ftalem7  23108  basellem5  23114  ppifi  23135  sqff1o  23212  1sgmprm  23230  logexprlim  23256  dchrelbasd  23270  dchr1re  23294  lgslem4  23330  lgsne0  23364  2sqlem9  23404  2sqlem10  23405  rpvmasumlem  23428  dchrisumlem1  23430  vmalogdivsum  23480  pntrlog2bndlem5  23522  ostth  23580  axlowdimlem16  23964  vdgrf  24602  eupath  24685  0blo  25411  nmlno0lem  25412  omlsilem  26024  pjoc1i  26053  nonbooli  26273  nmlnop0iALT  26618  unopbd  26638  leoprf2  26750  opsqrlem4  26766  opsqrlem5  26767  pjbdlni  26772  pjcmul1i  26824  sgnsf  27409  prsssdm  27563  ordtrestNEW  27567  esumcst  27739  sibf0  27944  sitgclcn  27954  sitgclre  27955  eulerpartlemgs2  27987  dstfrvclim1  28084  ballotlemfelz  28097  sgncl  28145  signstfveq0  28202  subfacp1lem3  28294  rellyscon  28364  cvmlift2lem9  28424  prodrblem  28666  fprodcvg  28667  prodmolem2a  28671  zprod  28674  fprodntriv  28679  prodss  28684  fprodss  28685  binomfallfac  28768  bdayelon  29045  bpoly1  29418  bpoly2  29424  bpoly3  29425  ordcmp  29517  voliunnfl  29663  mbfresfi  29666  itg2addnclem2  29672  bddiblnc  29690  dvasin  29708  heiborlem4  29941  heiborlem6  29943  wepwsolem  30619  flcidc  30756  iocmbl  30813  arearect  30816  lcmcl  30835  lhe4.4ex1a  30862  dvconstbi  30867  climneg  31180  cncfiooicc  31261  itgsinexplem1  31299  stoweidlem36  31364  wallispilem3  31395  fourierdlem93  31528  lincext2  32155