Theorem syl6eqel 2709

Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)

Hypotheses

Ref	Expression
syl6eqel.1	⊢ (𝜑 → 𝐴 = 𝐵)
syl6eqel.2	⊢ 𝐵 ∈ 𝐶

Assertion

Ref	Expression
syl6eqel	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem syl6eqel

Step	Hyp	Ref	Expression
1		syl6eqel.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		syl6eqel.2	. . 3 ⊢ 𝐵 ∈ 𝐶
3	2	a1i 11	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
4	1, 3	eqeltrd 2701	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1483   ∈ wcel 1990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-clel 2618

This theorem is referenced by:  syl6eqelr  2710  csbexg  4792  unisn2  4794  class2set  4832  snexALT  4852  snex  4908  prex  4909  onun2i  5843  iotaex  5868  fvrn0  6216  f0cli  6370  funsneqop  6418  fmptsng  6434  fmptsnd  6435  elimdelov  6736  ovima0  6813  ndmovcl  6819  caovmo  6871  soex  7109  zfrep6  7134  1st2ndb  7206  wfrlem17  7431  smofvon2  7453  tz7.44-2  7503  oesuclem  7605  omcl  7616  oecl  7617  nnmcl  7692  nnecl  7693  ixpexg  7932  resixpfo  7946  en1b  8024  xpsnen  8044  nnunifi  8211  xpfi  8231  fsuppun  8294  0fsupp  8297  oiexg  8440  hartogslem1  8447  cantnfvalf  8562  rankdmr1  8664  rankr1c  8684  numwdom  8882  alephon  8892  isfin5  9121  sdom2en01  9124  isf32lem9  9183  hsmexlem9  9247  iundom2g  9362  gchxpidm  9491  r1tskina  9604  tskmcl  9663  recmulnq  9786  recclnq  9788  genpelv  9822  un0mulcl  11327  znegcl  11412  zeo  11463  eqreznegel  11774  xnegcl  12044  xnn0xaddcl  12066  ioorebas  12275  modid0  12696  2txmodxeq0  12730  fzofi  12773  expcllem  12871  m1expcl2  12882  faclbnd4lem3  13082  bccl  13109  hasheq0  13154  hashrabrsn  13161  fnfz0hashnn0  13232  fnfzo0hashnn0  13235  ccat2s1p1  13405  cshwcl  13544  relexpaddg  13793  abs00bd  14031  iserge0  14391  sumrblem  14442  fsumcvg  14443  summolem2a  14446  sumss  14455  fsumss  14456  fsumcvg2  14458  sumsplit  14499  binom  14562  bcxmas  14567  geomulcvg  14607  prodrblem  14659  fprodcvg  14660  prodmolem2a  14664  zprod  14667  fprodntriv  14672  prodss  14677  fprodss  14678  binomfallfac  14772  bpoly1  14782  bpoly2  14788  bpoly3  14789  ruclem6  14964  smupf  15200  gcdcl  15228  lcmcl  15314  lcmfcl  15341  pcxcl  15565  pcmptcl  15595  infpnlem2  15615  zgz  15637  4sqlem2  15653  4sqlem19  15667  vdwapval  15677  hashbc0  15709  ramcl2  15720  0ramcl  15727  ramcl  15733  isstruct2  15867  imasval  16171  imasbas  16172  imasds  16173  imasplusg  16177  imasmulr  16178  imasvsca  16180  imasip  16181  imasle  16183  qusaddvallem  16211  qusaddflem  16212  qusaddval  16213  qusaddf  16214  qusmulval  16215  qusmulf  16216  mreexexlem3d  16306  sscpwex  16475  fullresc  16511  estrres  16779  evlfcl  16862  ipopos  17160  gsumress  17276  submnd0  17320  qusgrp2  17533  issubg2  17609  torsubg  18257  frgpnabllem1  18276  lt6abl  18296  ablfaclem3  18486  ablfac2  18488  srgbinomlem3  18542  ringidss  18577  qusring2  18620  isdrngd  18772  mptscmfsupp0  18928  islss3  18959  lspsnel  19003  lspprel  19094  znf1o  19900  frgpcyg  19922  cnmsgnsubg  19923  phlpropd  20000  cssval  20026  iscss  20027  dsmm0cl  20084  uvcvvcl  20126  m1detdiag  20403  m2detleiblem1  20430  pmatcollpw3fi1lem1  20591  indistopon  20805  indiscld  20895  restbas  20962  ordttopon  20997  iocpnfordt  21019  icomnfordt  21020  lecldbas  21023  fiuncmp  21207  cmpfi  21211  conncompid  21234  dissnlocfin  21332  elpt  21375  xkotop  21391  xkouni  21402  xkohaus  21456  xkoptsub  21457  imastopn  21523  filconn  21687  cfinufil  21732  alexsublem  21848  alexsub  21849  alexsubALTlem4  21854  distgp  21903  indistgp  21904  ssblps  22227  ssbl  22228  xmeter  22238  nmoi  22532  nmoeq0  22540  0nghm  22545  idnghm  22547  icccld  22570  iocmnfcld  22572  blssioo  22598  xrtgioo  22609  xrsxmet  22612  icccmp  22628  pcopt  22822  pcopt2  22823  elpi1  22845  cmetcaulem  23086  ishl2  23166  rrxmvallem  23187  ovolcl  23246  ovolunlem1a  23264  ovolunnul  23268  ovoliunnul  23275  ioombl1  23330  icombl  23332  ioombl  23333  iccmbl  23334  iccvolcl  23335  ovolioo  23336  ioovolcl  23338  ioorcl  23345  uniioovol  23347  uniioombllem2a  23350  uniioombllem4  23354  uniioombllem5  23355  vitalilem1  23376  vitalilem1OLD  23377  vitalilem5  23381  mbfconstlem  23396  mbfima  23399  mbfid  23403  ismbf2d  23408  mbfss  23413  mbfmulc2lem  23414  i1fd  23448  itg1addlem2  23464  itg1addlem4  23466  itg1addlem5  23467  i1fmulc  23470  itg2l  23496  itg2cl  23499  ibl0  23553  iblrelem  23557  iblpos  23559  iblss2  23572  bddmulibl  23605  recnperf  23669  ply1remlem  23922  fta1glem1  23925  fta1g  23927  elply  23951  plypf1  23968  coefv0  24004  coemulc  24011  fta1  24063  elqaalem2  24075  aannenlem2  24084  aalioulem3  24089  taylfvallem1  24111  tayl0  24116  ulm0  24145  logtayl  24406  atanrecl  24638  atanbnd  24653  harmonicbnd3  24734  ftalem7  24805  basellem5  24811  ppifi  24832  sqff1o  24908  1sgmprm  24924  logexprlim  24950  dchrelbasd  24964  dchr1re  24988  lgslem4  25025  lgsne0  25060  2sqlem9  25152  2sqlem10  25153  rpvmasumlem  25176  dchrisumlem1  25178  vmalogdivsum  25228  pntrlog2bndlem5  25270  ostth  25328  tgcgr4  25426  axlowdimlem16  25837  fusgrfisbase  26220  vtxdg0e  26370  rgrusgrprc  26485  clwwlksnfi  26913  trlsegvdeglem7  27086  eulerpathpr  27100  numclwwlkffin0  27215  0blo  27647  nmlno0lem  27648  omlsilem  28261  pjoc1i  28290  nonbooli  28510  nmlnop0iALT  28854  unopbd  28874  leoprf2  28986  opsqrlem4  29002  opsqrlem5  29003  pjbdlni  29008  pjcmul1i  29060  prsssdm  29963  ordtrestNEW  29967  esumpad  30117  esumpad2  30118  esumcst  30125  esumrnmpt2  30130  sibf0  30396  sitgclcn  30406  sitgclre  30407  eulerpartlemgs2  30442  dstfrvclim1  30539  ballotlemfelz  30552  sgncl  30600  signstfveq0  30654  breprexp  30711  subfacp1lem3  31164  rellysconn  31233  cvmlift2lem9  31293  ordcmp  32446  finxpreclem4  33231  poimirlem16  33425  poimirlem17  33426  voliunnfl  33453  mbfresfi  33456  itg2addnclem2  33462  bddiblnc  33480  dvasin  33496  heiborlem4  33613  heiborlem6  33615  wepwsolem  37612  flcidc  37744  iocmbl  37798  arearect  37801  briunov2uz  37990  eliunov2uz  37991  frege124d  38053  frege129d  38055  frege92  38249  lhe4.4ex1a  38528  dvconstbi  38533  binomcxplemnn0  38548  binomcxplemnotnn0  38555  infxr  39583  infleinflem2  39587  climneg  39842  cncfiooicc  40107  itgsinexplem1  40169  volioof  40204  stoweidlem36  40253  wallispilem3  40284  fourierdlem93  40416  fouriersw  40448  fouriercn  40449  etransclem16  40467  etransclem33  40484  sge0reuz  40664  nnfoctbdjlem  40672  hoidmvlelem3  40811  fmtnofz04prm  41489  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  sprsymrelfvlem  41740  lincext2  42244  blennn0elnn  42371