Theorem syl6eqel 2516

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

Syntax hints:   -> wi 4   = wceq 1437   e. wcel 1867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-ext 2398

This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-cleq 2412  df-clel 2415

This theorem is referenced by:  syl6eqelr  2517  csbexg  4551  unisn2  4553  class2set  4584  snexALT  4603  snex  4655  prex  4656  onun2i  5549  iotaex  5574  fvrn0  5895  f0cli  6040  fmptsng  6092  fmptsnd  6093  elimdelov  6378  ovima0  6454  ndmovcl  6460  caovmo  6512  soex  6742  zfrep6  6767  1st2ndb  6837  wfrlem17  7052  smofvon2  7075  tz7.44-2  7125  oesuclem  7227  omcl  7238  oecl  7239  nnmcl  7313  nnecl  7314  ixpexg  7546  resixpfo  7560  en1b  7636  xpsnen  7654  nnunifi  7820  xpfi  7840  fsuppun  7900  0fsupp  7903  oiexg  8048  hartogslem1  8055  cantnfvalf  8167  rankdmr1  8269  rankr1c  8289  numwdom  8486  alephon  8496  isfin5  8725  sdom2en01  8728  isf32lem9  8787  hsmexlem9  8851  iundom2g  8961  gchxpidm  9090  r1tskina  9203  tskmcl  9262  recmulnq  9385  recclnq  9387  genpelv  9421  un0mulcl  10900  znegcl  10968  zeo  11017  eqreznegel  11245  xnegcl  11502  ioorebas  11732  modid0  12115  modidmul0OLD  12116  2txmodxeq0  12143  fzofi  12180  expcllem  12276  m1expcl2  12287  faclbnd4lem3  12473  bccl  12500  hasheq0  12537  hashrabrsn  12544  hashimarn  12601  ccat2s1p1  12742  cshwcl  12881  relexpaddg  13095  abs00bd  13333  iserge0  13702  sumrblem  13755  fsumcvg  13756  summolem2a  13759  sumss  13768  fsumss  13769  fsumcvg2  13771  sumsplit  13807  binom  13866  bcxmas  13871  geomulcvg  13910  prodrblem  13961  fprodcvg  13962  prodmolem2a  13966  zprod  13969  fprodntriv  13974  prodss  13979  fprodss  13980  binomfallfac  14072  bpoly1  14082  bpoly2  14088  bpoly3  14089  ruclem6  14265  smupf  14430  gcdcl  14458  lcmcl  14544  lcmfcl  14579  pcxcl  14788  pcmptcl  14814  infpnlem2  14833  zgz  14855  4sqlem2  14871  4sqlem19  14891  vdwapval  14901  hashbc0  14935  ramcl2  14951  ramcl2OLD  14952  0ramcl  14959  ramcl  14965  isstruct2  15108  imasval  15389  imasvalOLD  15390  imasbas  15391  imasds  15392  imasplusg  15396  imasmulr  15397  imasvsca  15399  imasip  15400  imasle  15402  imasbasOLD  15403  imasdsOLD  15404  qusaddvallem  15435  qusaddflem  15436  qusaddval  15437  qusaddf  15438  qusmulval  15439  qusmulf  15440  mreexexlem3d  15530  sscpwex  15698  fullresc  15734  estrres  16002  evlfcl  16085  ipopos  16384  gsumress  16497  submnd0  16544  qusgrp2  16782  issubg2  16810  torsubg  17470  frgpnabllem1  17487  lt6abl  17507  ablfaclem3  17698  ablfac2  17700  srgbinomlem3  17753  ringidss  17785  qusring2  17826  isdrngd  17978  mptscmfsupp0  18131  islss3  18160  lspsnel  18204  lspprel  18295  znf1o  19099  frgpcyg  19121  cnmsgnsubg  19122  phlpropd  19199  cssval  19222  iscss  19223  dsmm0cl  19280  uvcvvcl  19322  m1detdiag  19599  m2detleiblem1  19626  pmatcollpw3fi1lem1  19787  indistopon  19993  indiscld  20084  restbas  20151  ordttopon  20186  iocpnfordt  20208  icomnfordt  20209  lecldbas  20212  fiuncmp  20396  cmpfi  20400  concompid  20423  dissnlocfin  20521  elpt  20564  xkotop  20580  xkouni  20591  xkohaus  20645  xkoptsub  20646  imastopn  20712  filcon  20875  cfinufil  20920  alexsublem  21036  alexsub  21037  alexsubALTlem4  21042  distgp  21091  indistgp  21092  ssblps  21414  ssbl  21415  xmeter  21425  nmoi  21710  nmoiOLD  21726  nmoeq0  21734  0nghm  21739  idnghm  21741  icccld  21764  iocmnfcld  21766  blssioo  21790  xrtgioo  21801  xrsxmet  21804  icccmp  21820  pcopt  22030  pcopt2  22031  elpi1  22053  cmetcaulem  22235  ishl2  22314  rrxmvallem  22335  ovolcl  22408  ovolunlem1a  22426  ovolunnul  22430  ovoliunnul  22437  ioombl1  22492  icombl  22494  ioombl  22495  iccmbl  22496  iccvolcl  22497  ovolioo  22498  ioovolcl  22499  ioorcl  22506  ioorclOLD  22511  uniioovol  22513  uniioombllem2a  22516  uniioombllem4  22521  uniioombllem5  22522  vitalilem1  22543  vitalilem5  22547  mbfconstlem  22562  mbfima  22565  mbfid  22569  ismbf2d  22574  mbfss  22579  mbfmulc2lem  22580  i1fd  22616  itg1addlem2  22632  itg1addlem4  22634  itg1addlem5  22635  i1fmulc  22638  itg2l  22664  itg2cl  22667  ibl0  22721  iblrelem  22725  iblpos  22727  iblss2  22740  bddmulibl  22773  recnperf  22837  ply1remlem  23090  fta1glem1  23093  fta1g  23095  elply  23126  plypf1  23143  coefv0  23179  coemulc  23186  fta1  23238  elqaalem2  23250  elqaalem2OLD  23253  aannenlem2  23262  aalioulem3  23267  taylfvallem1  23289  tayl0  23294  ulm0  23323  logtayl  23582  atanrecl  23814  atanbnd  23829  harmonicbnd3  23910  ftalem7  23982  basellem5  23988  ppifi  24009  sqff1o  24086  1sgmprm  24104  logexprlim  24130  dchrelbasd  24144  dchr1re  24168  lgslem4  24204  lgsne0  24238  2sqlem9  24278  2sqlem10  24279  rpvmasumlem  24302  dchrisumlem1  24304  vmalogdivsum  24354  pntrlog2bndlem5  24396  ostth  24454  tgcgr4  24553  axlowdimlem16  24964  vdgrf  25602  eupath  25685  0blo  26409  nmlno0lem  26410  omlsilem  27031  pjoc1i  27060  nonbooli  27280  nmlnop0iALT  27624  unopbd  27644  leoprf2  27756  opsqrlem4  27772  opsqrlem5  27773  pjbdlni  27778  pjcmul1i  27830  prsssdm  28712  ordtrestNEW  28716  esumpad  28865  esumpad2  28866  esumcst  28873  esumrnmpt2  28878  sibf0  29156  sitgclcn  29166  sitgclre  29167  eulerpartlemgs2  29202  dstfrvclim1  29299  ballotlemfelz  29312  sgncl  29398  signstfveq0  29455  subfacp1lem3  29894  rellyscon  29963  cvmlift2lem9  30023  bdayelon  30555  ordcmp  31093  poimirlem16  31864  poimirlem17  31865  voliunnfl  31892  mbfresfi  31895  itg2addnclem2  31902  bddiblnc  31920  dvasin  31936  heiborlem4  32054  heiborlem6  32056  wepwsolem  35814  flcidc  35954  iocmbl  36011  arearect  36014  briunov2uz  36144  eliunov2uz  36145  frege124d  36207  frege129d  36209  frege92  36403  lhe4.4ex1a  36530  dvconstbi  36535  binomcxplemnn0  36550  binomcxplemnotnn0  36557  climneg  37476  cncfiooicc  37559  itgsinexplem1  37617  stoweidlem36  37684  wallispilem3  37716  fourierdlem93  37850  fouriersw  37882  fouriercn  37883  etransclem16  37902  etransclem33  37919  nnfoctbdjlem  38023  nnsum4primeseven  38515  nnsum4primesevenALTV  38516  funsneqop  38630  lincext2  39312  blennn0elnn  39453