Theorem syl6eqel 2539

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

Syntax hints:   -> wi 4   = wceq 1383   e. wcel 1804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1600  df-cleq 2435  df-clel 2438

This theorem is referenced by:  syl6eqelr  2540  csbexg  4569  unisn2  4573  class2set  4604  snexALT  4623  snex  4678  prex  4679  onun2i  4983  iotaex  5558  fvrn0  5878  f0cli  6027  fmptsng  6077  fmptsnd  6078  elimdelov  6363  ovima0  6439  ndmovcl  6445  caovmo  6497  soex  6728  zfrep6  6753  1st2ndb  6823  smofvon2  7029  tz7.44-2  7075  oesuclem  7177  omcl  7188  oecl  7189  nnmcl  7263  nnecl  7264  ixpexg  7495  resixpfo  7509  en1b  7585  xpsnen  7603  nnunifi  7773  xpfi  7793  fsuppun  7850  0fsupp  7853  oiexg  7963  hartogslem1  7970  noinfepOLD  8080  cantnfvalf  8087  rankdmr1  8222  rankr1c  8242  numwdom  8443  alephon  8453  isfin5  8682  sdom2en01  8685  isf32lem9  8744  hsmexlem9  8808  iundom2g  8918  gchxpidm  9050  r1tskina  9163  tskmcl  9222  recmulnq  9345  recclnq  9347  genpelv  9381  un0mulcl  10837  znegcl  10906  zeo  10955  eqreznegel  11177  xnegcl  11422  ioorebas  11636  modid0  12002  modidmul0  12003  2txmodxeq0  12028  fzofi  12065  expcllem  12158  m1expcl2  12169  faclbnd4lem3  12354  bccl  12381  hasheq0  12414  hashrabrsn  12421  hashimarn  12477  ccat2s1p1  12613  cshwcl  12750  abs00bd  13105  iserge0  13464  sumrblem  13514  fsumcvg  13515  summolem2a  13518  sumss  13527  fsumss  13528  fsumcvg2  13530  sumsplit  13564  binom  13623  bcxmas  13628  geomulcvg  13666  prodrblem  13717  fprodcvg  13718  prodmolem2a  13722  zprod  13725  fprodntriv  13730  prodss  13735  fprodss  13736  ruclem6  13949  smupf  14109  gcdcl  14136  pcxcl  14365  pcmptcl  14391  infpnlem2  14410  zgz  14432  4sqlem2  14448  4sqlem19  14462  vdwapval  14472  hashbc0  14504  ramcl2  14515  0ramcl  14522  ramcl  14528  isstruct2  14622  imasval  14889  imasbas  14890  imasds  14891  imasplusg  14895  imasmulr  14896  imasvsca  14898  imasip  14899  imasle  14901  qusaddvallem  14929  qusaddflem  14930  qusaddval  14931  qusaddf  14932  qusmulval  14933  qusmulf  14934  mreexexlem3d  15024  sscpwex  15165  fullresc  15198  evlfcl  15469  ipopos  15768  gsumress  15881  submnd0  15928  qusgrp2  16166  issubg2  16194  torsubg  16838  frgpnabllem1  16855  lt6abl  16875  ablfaclem3  17116  ablfac2  17118  srgbinomlem3  17171  ringidss  17203  qusring2  17247  isdrngd  17399  mptscmfsupp0  17554  islss3  17583  lspsnel  17627  lspprel  17718  znf1o  18567  frgpcyg  18589  cnmsgnsubg  18590  phlpropd  18667  cssval  18690  iscss  18691  dsmm0cl  18748  uvcvvcl  18795  m1detdiag  19076  m2detleiblem1  19103  pmatcollpw3fi1lem1  19264  indistopon  19479  indiscld  19569  restbas  19636  ordttopon  19671  iocpnfordt  19693  icomnfordt  19694  lecldbas  19697  fiuncmp  19881  cmpfi  19885  concompid  19909  dissnlocfin  20007  elpt  20050  xkotop  20066  xkouni  20077  xkohaus  20131  xkoptsub  20132  imastopn  20198  filcon  20361  cfinufil  20406  alexsublem  20521  alexsub  20522  alexsubALTlem4  20527  distgp  20575  indistgp  20576  ssblps  20902  ssbl  20903  xmeter  20913  nmoi  21212  nmoeq0  21220  0nghm  21225  idnghm  21227  icccld  21251  iocmnfcld  21253  blssioo  21277  xrtgioo  21288  xrsxmet  21291  icccmp  21307  pcopt  21499  pcopt2  21500  elpi1  21522  cmetcaulem  21704  ishl2  21787  rrxmvallem  21808  ovolcl  21866  ovolunlem1a  21884  ovolunnul  21888  ovoliunnul  21895  ioombl1  21949  icombl  21951  ioombl  21952  iccmbl  21953  iccvolcl  21954  ovolioo  21955  ioovolcl  21956  ioorcl  21963  uniioovol  21965  uniioombllem2a  21968  uniioombllem4  21972  uniioombllem5  21973  vitalilem1  21994  vitalilem5  21998  mbfconstlem  22013  mbfima  22016  mbfid  22020  ismbf2d  22025  mbfss  22030  mbfmulc2lem  22031  i1fd  22065  itg1addlem2  22081  itg1addlem4  22083  itg1addlem5  22084  i1fmulc  22087  itg2l  22113  itg2cl  22116  ibl0  22170  iblrelem  22174  iblpos  22176  iblss2  22189  bddmulibl  22222  recnperf  22286  ply1remlem  22540  fta1glem1  22543  fta1g  22545  elply  22569  plypf1  22586  coefv0  22621  coemulc  22628  fta1  22680  elqaalem2  22692  aannenlem2  22701  aalioulem3  22706  taylfvallem1  22728  tayl0  22733  ulm0  22762  logtayl  23017  atanrecl  23218  atanbnd  23233  harmonicbnd3  23313  ftalem7  23328  basellem5  23334  ppifi  23355  sqff1o  23432  1sgmprm  23450  logexprlim  23476  dchrelbasd  23490  dchr1re  23514  lgslem4  23550  lgsne0  23584  2sqlem9  23624  2sqlem10  23625  rpvmasumlem  23648  dchrisumlem1  23650  vmalogdivsum  23700  pntrlog2bndlem5  23742  ostth  23800  axlowdimlem16  24236  vdgrf  24874  eupath  24957  0blo  25683  nmlno0lem  25684  omlsilem  26296  pjoc1i  26325  nonbooli  26545  nmlnop0iALT  26890  unopbd  26910  leoprf2  27022  opsqrlem4  27038  opsqrlem5  27039  pjbdlni  27044  pjcmul1i  27096  prsssdm  27876  ordtrestNEW  27880  esumcst  28048  sibf0  28253  sitgclcn  28263  sitgclre  28264  eulerpartlemgs2  28296  dstfrvclim1  28393  ballotlemfelz  28406  sgncl  28454  signstfveq0  28511  subfacp1lem3  28603  rellyscon  28673  cvmlift2lem9  28733  binomfallfac  29138  bdayelon  29415  bpoly1  29788  bpoly2  29794  bpoly3  29795  ordcmp  29887  voliunnfl  30033  mbfresfi  30036  itg2addnclem2  30042  bddiblnc  30060  dvasin  30078  heiborlem4  30285  heiborlem6  30287  wepwsolem  30962  flcidc  31099  iocmbl  31156  arearect  31159  lcmcl  31183  lhe4.4ex1a  31210  dvconstbi  31215  climneg  31524  cncfiooicc  31604  itgsinexplem1  31642  stoweidlem36  31707  wallispilem3  31738  fourierdlem93  31871  fouriersw  31903  fouriercn  31904  estrres  32494  lincext2  32791