Theorem syl6eqel 2521

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

Syntax hints:   -> wi 4   = wceq 1362   e. wcel 1755

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-cleq 2426  df-clel 2429

This theorem is referenced by:  syl6eqelr  2522  csbexg  4412  unisn2  4416  class2set  4447  snexALT  4466  snex  4521  prex  4522  onun2i  4821  iotaex  5386  fvrn0  5700  f0cli  5842  fmptsng  5887  elimdelov  6156  ndmovcl  6237  caovmo  6289  soex  6510  zfrep6  6534  1st2ndb  6603  smofvon2  6803  tz7.44-2  6849  oesuclem  6953  omcl  6964  oecl  6965  nnmcl  7039  nnecl  7040  ixpexg  7275  resixpfo  7289  en1b  7365  xpsnen  7383  nnunifi  7551  xpfi  7571  fsuppun  7627  0fsupp  7630  oiexg  7737  hartogslem1  7744  noinfepOLD  7854  cantnfvalf  7861  rankdmr1  7996  rankr1c  8016  numwdom  8217  alephon  8227  isfin5  8456  sdom2en01  8459  isf32lem9  8518  hsmexlem9  8582  iundom2g  8692  gchxpidm  8823  r1tskina  8936  tskmcl  8995  recmulnq  9120  recclnq  9122  genpelv  9156  un0mulcl  10601  znegcl  10667  zeo  10714  eqreznegel  10927  xnegcl  11170  ioorebas  11378  modid0  11716  modidmul0  11717  2txmodxeq0  11742  fzofi  11779  expcllem  11859  m1expcl2  11870  faclbnd4lem3  12054  bccl  12081  hasheq0  12114  hashrabrsn  12120  hashimarn  12183  cshwcl  12418  abs00bd  12763  iserge0  13121  sumrblem  13171  fsumcvg  13172  summolem2a  13175  sumss  13184  fsumss  13185  fsumcvg2  13187  sumsplit  13218  binom  13275  bcxmas  13280  geomulcvg  13318  ruclem6  13499  smupf  13656  gcdcl  13683  pcxcl  13909  pcmptcl  13935  infpnlem2  13954  zgz  13976  4sqlem2  13992  4sqlem19  14006  vdwapval  14016  hashbc0  14048  ramcl2  14059  0ramcl  14066  ramcl  14072  isstruct2  14165  imasval  14431  imasbas  14432  imasds  14433  imasplusg  14437  imasmulr  14438  imasvsca  14440  imasip  14441  imasle  14443  divsaddvallem  14471  divsaddflem  14472  divsaddval  14473  divsaddf  14474  divsmulval  14475  divsmulf  14476  mreexexlem3d  14566  sscpwex  14710  fullresc  14743  evlfcl  15014  ipopos  15312  submnd0  15433  gsumress  15486  divsgrp2  15652  issubg2  15675  torsubg  16315  frgpnabllem1  16330  lt6abl  16350  ablfaclem3  16561  ablfac2  16563  rngidss  16606  divsrng2  16646  isdrngd  16780  islss3  16961  lspsnel  17005  lspprel  17096  znf1o  17825  frgpcyg  17847  cnmsgnsubg  17848  phlpropd  17925  cssval  17948  iscss  17949  dsmm0cl  18006  uvcvvcl  18053  m2detleiblem1  18271  indistopon  18446  indiscld  18536  restbas  18603  ordttopon  18638  iocpnfordt  18660  icomnfordt  18661  lecldbas  18664  fiuncmp  18848  cmpfi  18852  concompid  18876  elpt  18986  xkotop  19002  xkouni  19013  xkohaus  19067  xkoptsub  19068  imastopn  19134  filcon  19297  cfinufil  19342  alexsublem  19457  alexsub  19458  alexsubALTlem4  19463  distgp  19511  indistgp  19512  ssblps  19838  ssbl  19839  xmeter  19849  nmoi  20148  nmoeq0  20156  0nghm  20161  idnghm  20163  icccld  20187  iocmnfcld  20189  blssioo  20213  xrtgioo  20224  xrsxmet  20227  icccmp  20243  pcopt  20435  pcopt2  20436  elpi1  20458  cmetcaulem  20640  ishl2  20723  rrxmvallem  20744  ovolcl  20802  ovolunlem1a  20820  ovolunnul  20824  ovoliunnul  20831  ioombl1  20884  icombl  20886  ioombl  20887  iccmbl  20888  iccvolcl  20889  ovolioo  20890  ioovolcl  20891  ioorcl  20898  uniioovol  20900  uniioombllem2a  20903  uniioombllem4  20907  uniioombllem5  20908  vitalilem1  20929  vitalilem5  20933  mbfconstlem  20948  mbfima  20951  mbfid  20955  ismbf2d  20960  mbfss  20965  mbfmulc2lem  20966  i1fd  21000  itg1addlem2  21016  itg1addlem4  21018  itg1addlem5  21019  i1fmulc  21022  itg2l  21048  itg2cl  21051  ibl0  21105  iblrelem  21109  iblpos  21111  iblss2  21124  bddmulibl  21157  recnperf  21221  ply1remlem  21518  fta1glem1  21521  fta1g  21523  elply  21547  plypf1  21564  coefv0  21599  coemulc  21606  fta1  21658  elqaalem2  21670  aannenlem2  21679  aalioulem3  21684  taylfvallem1  21706  tayl0  21711  ulm0  21740  logtayl  21989  atanrecl  22190  atanbnd  22205  harmonicbnd3  22285  ftalem7  22300  basellem5  22306  ppifi  22327  sqff1o  22404  1sgmprm  22422  logexprlim  22448  dchrelbasd  22462  dchr1re  22486  lgslem4  22522  lgsne0  22556  2sqlem9  22596  2sqlem10  22597  rpvmasumlem  22620  dchrisumlem1  22622  vmalogdivsum  22672  pntrlog2bndlem5  22714  ostth  22772  axlowdimlem16  23025  vdgrf  23390  eupath  23424  0blo  24014  nmlno0lem  24015  omlsilem  24627  pjoc1i  24656  nonbooli  24876  nmlnop0iALT  25221  unopbd  25241  leoprf2  25353  opsqrlem4  25369  opsqrlem5  25370  pjbdlni  25375  pjcmul1i  25427  sgnsf  26015  prsssdm  26200  ordtrestNEW  26204  esumcst  26367  sibf0  26567  sitgclcn  26577  sitgclre  26578  eulerpartlemgs2  26610  dstfrvclim1  26707  ballotlemfelz  26720  sgncl  26768  signstfveq0  26825  subfacp1lem3  26917  rellyscon  26987  cvmlift2lem9  27047  prodrblem  27288  fprodcvg  27289  prodmolem2a  27293  zprod  27296  fprodntriv  27301  prodss  27306  fprodss  27307  binomfallfac  27390  bdayelon  27667  bpoly1  28040  bpoly2  28046  bpoly3  28047  ordcmp  28140  voliunnfl  28276  mbfresfi  28279  itg2addnclem2  28285  bddiblnc  28303  dvasin  28321  heiborlem4  28554  heiborlem6  28556  wepwsolem  29236  flcidc  29373  iocmbl  29430  arearect  29433  lhe4.4ex1a  29445  dvconstbi  29450  climneg  29626  itgsinexplem1  29637  stoweidlem36  29674  wallispilem3  29705  fmptsnd  30564  lincext2  30695