Theorem syl6eqel 2696

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 2688	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606

This theorem is referenced by:  syl6eqelr  2697  csbexg  4720  unisn2  4722  class2set  4758  snexALT  4778  snex  4835  prex  4836  onun2i  5760  iotaex  5785  fvrn0  6126  f0cli  6278  funsneqop  6323  fmptsng  6339  fmptsnd  6340  elimdelov  6634  ovima0  6711  ndmovcl  6717  caovmo  6769  soex  7002  zfrep6  7027  1st2ndb  7097  wfrlem17  7318  smofvon2  7340  tz7.44-2  7390  oesuclem  7492  omcl  7503  oecl  7504  nnmcl  7579  nnecl  7580  ixpexg  7818  resixpfo  7832  en1b  7910  xpsnen  7929  nnunifi  8096  xpfi  8116  fsuppun  8177  0fsupp  8180  oiexg  8323  hartogslem1  8330  cantnfvalf  8445  rankdmr1  8547  rankr1c  8567  numwdom  8765  alephon  8775  isfin5  9004  sdom2en01  9007  isf32lem9  9066  hsmexlem9  9130  iundom2g  9241  gchxpidm  9370  r1tskina  9483  tskmcl  9542  recmulnq  9665  recclnq  9667  genpelv  9701  un0mulcl  11204  znegcl  11289  zeo  11339  eqreznegel  11650  xnegcl  11918  xnn0xaddcl  11940  ioorebas  12146  modid0  12558  2txmodxeq0  12592  fzofi  12635  expcllem  12733  m1expcl2  12744  faclbnd4lem3  12944  bccl  12971  hasheq0  13015  hashrabrsn  13022  fnfz0hashnn0  13089  fnfzo0hashnn0  13092  ccat2s1p1  13257  cshwcl  13395  relexpaddg  13641  abs00bd  13879  iserge0  14239  sumrblem  14289  fsumcvg  14290  summolem2a  14293  sumss  14302  fsumss  14303  fsumcvg2  14305  sumsplit  14341  binom  14401  bcxmas  14406  geomulcvg  14446  prodrblem  14498  fprodcvg  14499  prodmolem2a  14503  zprod  14506  fprodntriv  14511  prodss  14516  fprodss  14517  binomfallfac  14611  bpoly1  14621  bpoly2  14627  bpoly3  14628  ruclem6  14803  smupf  15038  gcdcl  15066  lcmcl  15152  lcmfcl  15179  pcxcl  15403  pcmptcl  15433  infpnlem2  15453  zgz  15475  4sqlem2  15491  4sqlem19  15505  vdwapval  15515  hashbc0  15547  ramcl2  15558  0ramcl  15565  ramcl  15571  isstruct2  15704  imasval  15994  imasbas  15995  imasds  15996  imasplusg  16000  imasmulr  16001  imasvsca  16003  imasip  16004  imasle  16006  qusaddvallem  16034  qusaddflem  16035  qusaddval  16036  qusaddf  16037  qusmulval  16038  qusmulf  16039  mreexexlem3d  16129  sscpwex  16298  fullresc  16334  estrres  16602  evlfcl  16685  ipopos  16983  gsumress  17099  submnd0  17143  qusgrp2  17356  issubg2  17432  torsubg  18080  frgpnabllem1  18099  lt6abl  18119  ablfaclem3  18309  ablfac2  18311  srgbinomlem3  18365  ringidss  18400  qusring2  18443  isdrngd  18595  mptscmfsupp0  18751  islss3  18780  lspsnel  18824  lspprel  18915  znf1o  19719  frgpcyg  19741  cnmsgnsubg  19742  phlpropd  19819  cssval  19845  iscss  19846  dsmm0cl  19903  uvcvvcl  19945  m1detdiag  20222  m2detleiblem1  20249  pmatcollpw3fi1lem1  20410  indistopon  20615  indiscld  20705  restbas  20772  ordttopon  20807  iocpnfordt  20829  icomnfordt  20830  lecldbas  20833  fiuncmp  21017  cmpfi  21021  concompid  21044  dissnlocfin  21142  elpt  21185  xkotop  21201  xkouni  21212  xkohaus  21266  xkoptsub  21267  imastopn  21333  filcon  21497  cfinufil  21542  alexsublem  21658  alexsub  21659  alexsubALTlem4  21664  distgp  21713  indistgp  21714  ssblps  22037  ssbl  22038  xmeter  22048  nmoi  22342  nmoeq0  22350  0nghm  22355  idnghm  22357  icccld  22380  iocmnfcld  22382  blssioo  22406  xrtgioo  22417  xrsxmet  22420  icccmp  22436  pcopt  22630  pcopt2  22631  elpi1  22653  cmetcaulem  22894  ishl2  22974  rrxmvallem  22995  ovolcl  23053  ovolunlem1a  23071  ovolunnul  23075  ovoliunnul  23082  ioombl1  23137  icombl  23139  ioombl  23140  iccmbl  23141  iccvolcl  23142  ovolioo  23143  ioovolcl  23144  ioorcl  23151  uniioovol  23153  uniioombllem2a  23156  uniioombllem4  23160  uniioombllem5  23161  vitalilem1  23182  vitalilem1OLD  23183  vitalilem5  23187  mbfconstlem  23202  mbfima  23205  mbfid  23209  ismbf2d  23214  mbfss  23219  mbfmulc2lem  23220  i1fd  23254  itg1addlem2  23270  itg1addlem4  23272  itg1addlem5  23273  i1fmulc  23276  itg2l  23302  itg2cl  23305  ibl0  23359  iblrelem  23363  iblpos  23365  iblss2  23378  bddmulibl  23411  recnperf  23475  ply1remlem  23726  fta1glem1  23729  fta1g  23731  elply  23755  plypf1  23772  coefv0  23808  coemulc  23815  fta1  23867  elqaalem2  23879  aannenlem2  23888  aalioulem3  23893  taylfvallem1  23915  tayl0  23920  ulm0  23949  logtayl  24206  atanrecl  24438  atanbnd  24453  harmonicbnd3  24534  ftalem7  24605  basellem5  24611  ppifi  24632  sqff1o  24708  1sgmprm  24724  logexprlim  24750  dchrelbasd  24764  dchr1re  24788  lgslem4  24825  lgsne0  24860  2sqlem9  24952  2sqlem10  24953  rpvmasumlem  24976  dchrisumlem1  24978  vmalogdivsum  25028  pntrlog2bndlem5  25070  ostth  25128  tgcgr4  25226  axlowdimlem16  25637  vdgrf  26425  eupath  26508  0blo  27031  nmlno0lem  27032  omlsilem  27645  pjoc1i  27674  nonbooli  27894  nmlnop0iALT  28238  unopbd  28258  leoprf2  28370  opsqrlem4  28386  opsqrlem5  28387  pjbdlni  28392  pjcmul1i  28444  prsssdm  29291  ordtrestNEW  29295  esumpad  29444  esumpad2  29445  esumcst  29452  esumrnmpt2  29457  sibf0  29723  sitgclcn  29733  sitgclre  29734  eulerpartlemgs2  29769  dstfrvclim1  29866  ballotlemfelz  29879  sgncl  29927  signstfveq0  29980  subfacp1lem3  30418  rellyscon  30487  cvmlift2lem9  30547  bdayelon  31079  ordcmp  31616  finxpreclem4  32407  poimirlem16  32595  poimirlem17  32596  voliunnfl  32623  mbfresfi  32626  itg2addnclem2  32632  bddiblnc  32650  dvasin  32666  heiborlem4  32783  heiborlem6  32785  wepwsolem  36630  flcidc  36763  iocmbl  36817  arearect  36820  briunov2uz  37009  eliunov2uz  37010  frege124d  37072  frege129d  37074  frege92  37269  lhe4.4ex1a  37550  dvconstbi  37555  binomcxplemnn0  37570  binomcxplemnotnn0  37577  infxr  38524  infleinflem2  38528  climneg  38677  cncfiooicc  38780  itgsinexplem1  38845  volioof  38880  stoweidlem36  38929  wallispilem3  38960  fourierdlem93  39092  fouriersw  39124  fouriercn  39125  etransclem16  39143  etransclem33  39160  sge0reuz  39340  nnfoctbdjlem  39348  hoidmvlelem3  39487  fmtnofz04prm  40027  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  fusgrfisbase  40547  vtxdg0e  40689  rgrusgrprc  40789  clwwlksnfi  41220  trlsegvdeglem7  41394  eulerpathpr  41408  av-numclwwlkffin0  41513  lincext2  42038  blennn0elnn  42169