Theorem syl6eqel 2492

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

Syntax hints:   -> wi 4   = wceq 1649   e. wcel 1721

This theorem is referenced by:  syl6eqelr  2493  class2set  4327  snexALT  4345  snex  4365  prex  4366  onun2i  4656  unisn2  4670  soex  5278  iotaex  5394  fvrn0  5712  f0cli  5839  zfrep6  5927  elimdelov  6112  ndmovcl  6191  caovmo  6243  1st2ndb  6346  smofvon2  6577  tz7.44-2  6624  oesuclem  6728  omcl  6739  oecl  6740  nnmcl  6814  nnecl  6815  ixpexg  7045  resixpfo  7059  en1b  7134  xpsnen  7151  nnunifi  7317  xpfi  7337  oiexg  7460  hartogslem1  7467  noinfepOLD  7571  cantnfvalf  7576  cantnf0  7586  rankdmr1  7683  rankr1c  7703  numwdom  7896  alephon  7906  isfin5  8135  sdom2en01  8138  isf32lem9  8197  hsmexlem9  8261  iundom2g  8371  gchxpidm  8500  r1tskina  8613  tskmcl  8672  recmulnq  8797  recclnq  8799  genpelv  8833  un0mulcl  10210  znegcl  10269  zeo  10311  eqreznegel  10517  xnegcl  10755  ioorebas  10962  fzofi  11268  expcllem  11347  m1expcl2  11358  faclbnd4lem3  11541  bccl  11568  hasheq0  11599  hashrabrsn  11603  abs00bd  12051  iserge0  12409  sumrblem  12460  fsumcvg  12461  summolem2a  12464  zsum  12467  sumss  12473  fsumss  12474  fsumcvg2  12476  sumsplit  12507  binom  12564  bcxmas  12570  geomulcvg  12608  ruclem6  12789  smupf  12945  gcdcl  12972  pcxcl  13189  pcmptcl  13215  infpnlem2  13234  zgz  13256  4sqlem2  13272  4sqlem19  13286  vdwapval  13296  hashbc0  13328  ramcl2  13339  0ramcl  13346  ramcl  13352  isstruct2  13433  imasval  13692  imasbas  13693  imasds  13694  imasplusg  13698  imasmulr  13699  imasvsca  13701  imasle  13703  divsaddvallem  13731  divsaddflem  13732  divsaddval  13733  divsaddf  13734  divsmulval  13735  divsmulf  13736  mreexexlem3d  13826  sscpwex  13970  fullresc  14003  evlfcl  14274  ipopos  14541  submnd0  14680  gsumress  14732  divsgrp2  14891  issubg2  14914  torsubg  15424  frgpnabllem1  15439  lt6abl  15459  ablfaclem3  15600  ablfac2  15602  rngidss  15645  divsrng2  15681  isdrngd  15815  islss3  15990  lspsnel  16034  lspprel  16121  znf1o  16787  frgpcyg  16809  phlpropd  16841  cssval  16864  iscss  16865  indistopon  17020  indiscld  17110  restbas  17176  ordttopon  17211  iocpnfordt  17233  icomnfordt  17234  lecldbas  17237  fiuncmp  17421  cmpfi  17425  concompid  17447  elpt  17557  xkotop  17573  xkouni  17584  xkohaus  17638  xkoptsub  17639  imastopn  17705  filcon  17868  cfinufil  17913  alexsublem  18028  alexsub  18029  alexsubALTlem4  18034  distgp  18082  indistgp  18083  ssblps  18405  ssbl  18406  xmeter  18416  nmoi  18715  nmoeq0  18723  0nghm  18728  idnghm  18730  icccld  18754  iocmnfcld  18756  blssioo  18779  xrtgioo  18790  xrsxmet  18793  icccmp  18809  pcopt  19000  pcopt2  19001  elpi1  19023  cmetcaulem  19194  ishl2  19277  ovolcl  19327  ovolunlem1a  19345  ovolunnul  19349  ovoliunnul  19356  ioombl1  19409  icombl  19411  ioombl  19412  iccmbl  19413  iccvolcl  19414  ovolioo  19415  ioorcl  19422  uniioovol  19424  uniioombllem2a  19427  uniioombllem4  19431  uniioombllem5  19432  vitalilem1  19453  vitalilem5  19457  mbfconstlem  19474  mbfima  19477  mbfid  19481  ismbf2d  19486  mbfss  19491  mbfmulc2lem  19492  i1fd  19526  itg1addlem2  19542  itg1addlem4  19544  itg1addlem5  19545  i1fmulc  19548  itg2l  19574  itg2cl  19577  ibl0  19631  iblrelem  19635  iblpos  19637  iblss2  19650  bddmulibl  19683  recnperf  19745  ply1remlem  20038  fta1glem1  20041  fta1g  20043  elply  20067  plypf1  20084  coefv0  20119  coemulc  20126  fta1  20178  elqaalem2  20190  aannenlem2  20199  aalioulem3  20204  taylfvallem1  20226  tayl0  20231  ulm0  20260  logtayl  20504  atanrecl  20704  atanbnd  20719  harmonicbnd3  20799  ftalem7  20814  basellem5  20820  ppifi  20841  sqff1o  20918  1sgmprm  20936  logexprlim  20962  dchrelbasd  20976  dchr1re  21000  lgslem4  21036  lgsne0  21070  2sqlem9  21110  2sqlem10  21111  rpvmasumlem  21134  dchrisumlem1  21136  vmalogdivsum  21186  pntrlog2bndlem5  21228  ostth  21286  vdgrf  21622  eupath  21656  0blo  22246  nmlno0lem  22247  omlsilem  22857  pjoc1i  22886  nonbooli  23106  nmlnop0iALT  23451  unopbd  23471  leoprf2  23583  opsqrlem4  23599  opsqrlem5  23600  pjbdlni  23605  pjcmul1i  23657  esumcst  24408  sibf0  24602  sitgclcn  24611  sitgclre  24612  dstfrvclim1  24688  ballotlemfelz  24701  subfacp1lem3  24821  rellyscon  24891  cvmlift2lem9  24951  prodrblem  25208  fprodcvg  25209  prodmolem2a  25213  zprod  25216  fprodntriv  25221  prodss  25226  fprodss  25227  binomfallfac  25308  bdayelon  25548  axlowdimlem16  25800  bpoly1  26001  bpoly2  26007  bpoly3  26008  ordcmp  26101  voliunnfl  26149  mbfresfi  26152  itg2addnclem2  26156  bddiblnc  26174  heiborlem4  26413  heiborlem6  26415  wepwsolem  27006  dsmm0cl  27074  uvcvvcl  27104  flcidc  27247  cnmsgnsubg  27302  lhe4.4ex1a  27414  dvconstbi  27419  climneg  27603  ioovolcl  27609  itgsinexplem1  27615  stoweidlem36  27652  wallispilem3  27683  hashimarn  27994

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2397  df-clel 2400