Theorem syl6eqel 2537

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

Syntax hints:   -> wi 4   = wceq 1444   e. wcel 1887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-cleq 2444  df-clel 2447

This theorem is referenced by:  syl6eqelr  2538  csbexg  4537  unisn2  4539  class2set  4570  snexALT  4589  snex  4641  prex  4642  onun2i  5538  iotaex  5563  fvrn0  5887  f0cli  6033  fmptsng  6085  fmptsnd  6086  elimdelov  6372  ovima0  6448  ndmovcl  6454  caovmo  6506  soex  6736  zfrep6  6761  1st2ndb  6831  wfrlem17  7052  smofvon2  7075  tz7.44-2  7125  oesuclem  7227  omcl  7238  oecl  7239  nnmcl  7313  nnecl  7314  ixpexg  7546  resixpfo  7560  en1b  7637  xpsnen  7656  nnunifi  7822  xpfi  7842  fsuppun  7902  0fsupp  7905  oiexg  8050  hartogslem1  8057  cantnfvalf  8170  rankdmr1  8272  rankr1c  8292  numwdom  8490  alephon  8500  isfin5  8729  sdom2en01  8732  isf32lem9  8791  hsmexlem9  8855  iundom2g  8965  gchxpidm  9094  r1tskina  9207  tskmcl  9266  recmulnq  9389  recclnq  9391  genpelv  9425  un0mulcl  10904  znegcl  10972  zeo  11021  eqreznegel  11249  xnegcl  11506  ioorebas  11736  modid0  12122  modidmul0OLD  12123  2txmodxeq0  12150  fzofi  12187  expcllem  12283  m1expcl2  12294  faclbnd4lem3  12480  bccl  12507  hasheq0  12544  hashrabrsn  12551  hashimarn  12610  ccat2s1p1  12761  cshwcl  12900  relexpaddg  13116  abs00bd  13354  iserge0  13724  sumrblem  13777  fsumcvg  13778  summolem2a  13781  sumss  13790  fsumss  13791  fsumcvg2  13793  sumsplit  13829  binom  13888  bcxmas  13893  geomulcvg  13932  prodrblem  13983  fprodcvg  13984  prodmolem2a  13988  zprod  13991  fprodntriv  13996  prodss  14001  fprodss  14002  binomfallfac  14094  bpoly1  14104  bpoly2  14110  bpoly3  14111  ruclem6  14287  smupf  14452  gcdcl  14480  lcmcl  14566  lcmfcl  14601  pcxcl  14810  pcmptcl  14836  infpnlem2  14855  zgz  14877  4sqlem2  14893  4sqlem19  14913  vdwapval  14923  hashbc0  14957  ramcl2  14973  ramcl2OLD  14974  0ramcl  14981  ramcl  14987  isstruct2  15130  imasval  15411  imasvalOLD  15412  imasbas  15413  imasds  15414  imasplusg  15418  imasmulr  15419  imasvsca  15421  imasip  15422  imasle  15424  imasbasOLD  15425  imasdsOLD  15426  qusaddvallem  15457  qusaddflem  15458  qusaddval  15459  qusaddf  15460  qusmulval  15461  qusmulf  15462  mreexexlem3d  15552  sscpwex  15720  fullresc  15756  estrres  16024  evlfcl  16107  ipopos  16406  gsumress  16519  submnd0  16566  qusgrp2  16804  issubg2  16832  torsubg  17492  frgpnabllem1  17509  lt6abl  17529  ablfaclem3  17720  ablfac2  17722  srgbinomlem3  17775  ringidss  17807  qusring2  17848  isdrngd  18000  mptscmfsupp0  18153  islss3  18182  lspsnel  18226  lspprel  18317  znf1o  19122  frgpcyg  19144  cnmsgnsubg  19145  phlpropd  19222  cssval  19245  iscss  19246  dsmm0cl  19303  uvcvvcl  19345  m1detdiag  19622  m2detleiblem1  19649  pmatcollpw3fi1lem1  19810  indistopon  20016  indiscld  20107  restbas  20174  ordttopon  20209  iocpnfordt  20231  icomnfordt  20232  lecldbas  20235  fiuncmp  20419  cmpfi  20423  concompid  20446  dissnlocfin  20544  elpt  20587  xkotop  20603  xkouni  20614  xkohaus  20668  xkoptsub  20669  imastopn  20735  filcon  20898  cfinufil  20943  alexsublem  21059  alexsub  21060  alexsubALTlem4  21065  distgp  21114  indistgp  21115  ssblps  21437  ssbl  21438  xmeter  21448  nmoi  21733  nmoiOLD  21749  nmoeq0  21757  0nghm  21762  idnghm  21764  icccld  21787  iocmnfcld  21789  blssioo  21813  xrtgioo  21824  xrsxmet  21827  icccmp  21843  pcopt  22053  pcopt2  22054  elpi1  22076  cmetcaulem  22258  ishl2  22337  rrxmvallem  22358  ovolcl  22431  ovolunlem1a  22449  ovolunnul  22453  ovoliunnul  22460  ioombl1  22515  icombl  22517  ioombl  22518  iccmbl  22519  iccvolcl  22520  ovolioo  22521  ioovolcl  22522  ioorcl  22529  ioorclOLD  22534  uniioovol  22536  uniioombllem2a  22539  uniioombllem4  22544  uniioombllem5  22545  vitalilem1  22566  vitalilem5  22570  mbfconstlem  22585  mbfima  22588  mbfid  22592  ismbf2d  22597  mbfss  22602  mbfmulc2lem  22603  i1fd  22639  itg1addlem2  22655  itg1addlem4  22657  itg1addlem5  22658  i1fmulc  22661  itg2l  22687  itg2cl  22690  ibl0  22744  iblrelem  22748  iblpos  22750  iblss2  22763  bddmulibl  22796  recnperf  22860  ply1remlem  23113  fta1glem1  23116  fta1g  23118  elply  23149  plypf1  23166  coefv0  23202  coemulc  23209  fta1  23261  elqaalem2  23273  elqaalem2OLD  23276  aannenlem2  23285  aalioulem3  23290  taylfvallem1  23312  tayl0  23317  ulm0  23346  logtayl  23605  atanrecl  23837  atanbnd  23852  harmonicbnd3  23933  ftalem7  24005  basellem5  24011  ppifi  24032  sqff1o  24109  1sgmprm  24127  logexprlim  24153  dchrelbasd  24167  dchr1re  24191  lgslem4  24227  lgsne0  24261  2sqlem9  24301  2sqlem10  24302  rpvmasumlem  24325  dchrisumlem1  24327  vmalogdivsum  24377  pntrlog2bndlem5  24419  ostth  24477  tgcgr4  24576  axlowdimlem16  24987  vdgrf  25626  eupath  25709  0blo  26433  nmlno0lem  26434  omlsilem  27055  pjoc1i  27084  nonbooli  27304  nmlnop0iALT  27648  unopbd  27668  leoprf2  27780  opsqrlem4  27796  opsqrlem5  27797  pjbdlni  27802  pjcmul1i  27854  prsssdm  28723  ordtrestNEW  28727  esumpad  28876  esumpad2  28877  esumcst  28884  esumrnmpt2  28889  sibf0  29167  sitgclcn  29177  sitgclre  29178  eulerpartlemgs2  29213  dstfrvclim1  29310  ballotlemfelz  29323  sgncl  29409  signstfveq0  29466  subfacp1lem3  29905  rellyscon  29974  cvmlift2lem9  30034  bdayelon  30569  ordcmp  31107  finxpreclem4  31786  poimirlem16  31956  poimirlem17  31957  voliunnfl  31984  mbfresfi  31987  itg2addnclem2  31994  bddiblnc  32012  dvasin  32028  heiborlem4  32146  heiborlem6  32148  wepwsolem  35900  flcidc  36040  iocmbl  36097  arearect  36100  briunov2uz  36290  eliunov2uz  36291  frege124d  36353  frege129d  36355  frege92  36551  lhe4.4ex1a  36678  dvconstbi  36683  binomcxplemnn0  36698  binomcxplemnotnn0  36705  climneg  37689  cncfiooicc  37772  itgsinexplem1  37830  stoweidlem36  37897  wallispilem3  37929  fourierdlem93  38063  fouriersw  38095  fouriercn  38096  etransclem16  38115  etransclem33  38132  nnfoctbdjlem  38293  hoidmvlelem3  38419  nnsum4primeseven  38895  nnsum4primesevenALTV  38896  funsneqop  39024  xnn0xaddcl  39086  fusgrfisbase  39394  vtxdg0e  39534  rgrusgrprc  39604  pthsfval  39689  lincext2  40301  blennn0elnn  40441