Theorem syl6eleqr 2699

Description: A membership and equality inference. (Contributed by NM, 24-Apr-2005.)

Hypotheses

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

Assertion

Ref	Expression
syl6eleqr	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem syl6eleqr

Step	Hyp	Ref	Expression
1		syl6eleqr.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		syl6eleqr.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2619	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	syl6eleq 2698	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-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:  3eltr4g  2705  tpnzd  4257  brelrng  5276  elabrex  6405  fliftel1  6460  ovidig  6676  unielxp  7095  tfrlem11  7371  rdglim  7409  seqomlem4  7435  2oconcl  7470  ecopqsi  7691  erov  7731  eroprf  7732  sbthlem2  7956  dffi3  8220  ixpiunwdom  8379  cantnfcl  8447  r1lim  8518  rankwflemb  8539  pwwf  8553  unwf  8556  rankwflem  8561  uniwf  8565  rankpwi  8569  rankr1g  8578  r1pw  8591  r1rankid  8605  rankuni  8609  cardlim  8681  infxpenlem  8719  alephfp  8814  cfsmolem  8975  alephsing  8981  hsmexlem4  9134  axdc3lem2  9156  numth3  9175  iunfo  9240  konigthlem  9269  iunctb  9275  canthwelem  9351  canthwe  9352  r1limwun  9437  inar1  9476  inatsk  9479  gruina  9519  grur1  9521  tskmval  9540  tskmcl  9542  pinq  9628  dmrecnq  9669  addclsr  9783  mulclsr  9784  axaddf  9845  axmulf  9846  peano2nn  10909  uztrn2  11581  eluz2nn  11602  peano2uzs  11618  uzsupss  11656  uzsup  12524  uzrdgfni  12619  uzrdgsuci  12621  fsuppmapnn0fiub  12652  seqf  12684  ser0  12715  bcm1k  12964  bcp1nk  12966  bcpasc  12970  hashprdifel  13047  fz1isolem  13102  pr2pwpr  13116  ccatrn  13225  ccats1val2  13256  swrdccatin12lem3  13341  rexuzre  13940  limsupgre  14060  climconst  14122  rlimclim1  14124  climrlim2  14126  clim2ser  14233  clim2ser2  14234  iserex  14235  isermulc2  14236  iserle  14238  isercolllem3  14245  isercoll2  14247  climsup  14248  iseraltlem2  14261  iseraltlem3  14262  zsum  14296  isumclim3  14332  isumadd  14340  fsump1i  14342  iserabs  14388  cvgcmp  14389  cvgcmpub  14390  cvgcmpce  14391  abscvgcvg  14392  isumshft  14410  isumsplit  14411  isum1p  14412  isumrpcl  14414  isumsup2  14417  climcndslem1  14420  cvgrat  14454  clim2prod  14459  clim2div  14460  prodf1  14462  ntrivcvgn0  14469  ntrivcvgtail  14471  fprodntriv  14511  fprodabs  14543  fprodeq0  14544  iprodclim3  14570  iprodmul  14573  ef0lem  14648  fprodefsum  14664  rpnnen2lem3  14784  dvdsflip  14877  fzo0dvdseq  14883  bitsinv1  15002  smupval  15048  smueqlem  15050  seq1st  15122  algr0  15123  prmind2  15236  crth  15321  eulerthlem2  15325  prmdiv  15328  pockthlem  15447  pockthg  15448  unbenlem  15450  prmunb  15456  prmgaplem7  15599  strfv2d  15733  imasvscaval  16021  oppccatid  16202  epii  16226  fthepi  16411  funcestrcsetclem3  16605  funcsetcestrclem3  16619  yon12  16728  yon2  16729  yonedalem4c  16740  yonedalem22  16741  yonedalem3b  16742  yonedainv  16744  acsmapd  17001  mgm2nsgrplem1  17228  mgm2nsgrplem2  17229  mgm2nsgrplem3  17230  sgrp2nmndlem1  17233  sgrp2rid2  17236  cntrsubgnsg  17596  pmtrrn  17700  gexcl3  17825  efgi  17955  efgi2  17961  efgs1b  17972  efgredlemg  17978  efgredlemd  17980  frgpnabllem1  18099  cycsubgcyg  18125  gsumzaddlem  18144  dprdwd  18233  dprd2da  18264  lsppratlem3  18970  lsppratlem4  18971  lbsextlem2  18980  lidl0  19040  lidl1  19041  mplsubrglem  19260  mpfconst  19351  mpfproj  19352  mpfind  19357  pf1const  19531  pf1id  19532  mpfpf1  19536  pf1mpf  19537  domnchr  19699  znf1o  19719  madetsumid  20086  slesolex  20307  pmatcoe1fsupp  20325  mat2pmatbas0  20351  pmatcollpw  20405  pm2mpf1  20423  isclo  20701  indiscld  20705  restntr  20796  ordtbaslem  20802  ordtbas2  20805  lmconst  20875  lmss  20912  concompid  21044  2ndcomap  21071  locfincmp  21139  comppfsc  21145  xkouni  21212  txcls  21217  ptclsg  21228  uptx  21238  txindis  21247  tx1stc  21263  cnmpt1res  21289  tgqtop  21325  uffix  21535  cnpflf2  21614  ptcmplem2  21667  ptcmplem4  21669  tgpconcomp  21726  tsmsfbas  21741  fmucnd  21906  prdsxmetlem  21983  imasdsf1olem  21988  prdsbl  22106  blcvx  22409  xrsmopn  22423  xrge0tsms  22445  metdcn2  22450  expcncf  22533  cnmpt2pc  22535  icchmeo  22548  iccpnfhmeo  22552  cnheibor  22562  evth  22566  evth2  22567  lebnumlem2  22569  lebnumii  22573  reparphti  22605  cfilfcls  22880  minveclem2  23005  minveclem3  23008  minveclem4  23011  ovoliunlem1  23077  ovolicc1  23091  iundisj  23123  volsup  23131  uniioombllem3  23159  vitalilem2  23184  vitalilem3  23185  mbfsup  23237  mbfinf  23238  mbflimsup  23239  itg2monolem1  23323  limcflflem  23450  limccnp  23461  limccnp2  23462  dvidlem  23485  dvn2bss  23499  cpnres  23506  dvcobr  23515  dvrec  23524  c1liplem1  23563  dvcnvrelem2  23585  dvfsumrlimf  23592  dvfsumlem1  23593  dvfsumlem2  23594  dvfsumlem3  23595  dvfsumlem4  23596  dvfsumrlim  23598  dvfsum2  23601  coeeulem  23784  coeid3  23800  plycn  23821  dvntaylp  23929  taylthlem1  23931  taylthlem2  23932  ulm2  23943  ulmshftlem  23947  ulmshft  23948  ulm0  23949  ulmcn  23957  ulmdvlem3  23960  ulmdv  23961  mtest  23962  mtestbdd  23963  dvradcnv  23979  psercn2  23981  psercn  23984  pserdv  23987  abelth  23999  efif1olem2  24093  efif1olem4  24095  efifo  24097  eff1olem  24098  logcn  24193  dvloglem  24194  cxpcn3  24289  resqrtcn  24290  sqrtcn  24291  logbleb  24321  logblt  24322  asinneg  24413  atanlogsub  24443  atanbnd  24453  ressatans  24461  leibpilem2  24468  xrlimcnp  24495  efrlim  24496  scvxcvx  24512  ppiub  24729  chtub  24737  logexprlim  24750  lgseisenlem1  24900  rplogsumlem1  24973  rplogsumlem2  24974  dchrisumlem2  24979  dchrisum0flb  24999  logdivbnd  25045  pntlem3  25098  tgcgr4  25226  ltgov  25292  f1otrg  25551  eengtrkg  25665  nbgraf1olem3  25972  cusgrares  26001  wlknwwlknfun  26238  eupap1  26503  minvecolem1  27114  minvecolem2  27115  minvecolem4  27120  htthlem  27158  5oalem2  27898  3oalem2  27906  iundisjf  28784  xppreima  28829  xppreima2  28830  dfcnv2  28859  xrge0tsmsd  29116  rhmopp  29150  pmtrto1cl  29180  psgnfzto1stlem  29181  fzto1stfv1  29182  fzto1st  29184  fzto1stinvn  29185  psgnfzto1st  29186  smatlem  29191  smatcl  29196  tpr2rico  29286  xrmulc1cn  29304  xrge0mulc1cn  29315  esumpfinvallem  29463  ldgenpisyslem1  29553  dynkin  29557  brfae  29638  sxbrsigalem3  29661  dya2icoseg2  29667  omsmeas  29712  sibfof  29729  sseqmw  29780  sseqf  29781  sseqp1  29784  fiblem  29787  fibp1  29790  probfinmeasbOLD  29817  bnj1379  30155  subfacp1lem5  30420  subfacp1lem6  30421  cvxpcon  30478  cvxscon  30479  cvmliftlem6  30526  cvmliftlem8  30528  cvmliftlem10  30530  cvmlift2lem6  30544  cvmlift2lem11  30549  cvmlift2lem12  30550  msubff  30681  msubco  30682  elmsta  30699  msubff1  30707  mvhf  30709  msubvrs  30711  iprodefisumlem  30879  nobndlem2  31092  nobndlem6  31096  nofulllem3  31103  filnetlem3  31545  knoppcnlem10  31662  knoppcnlem11  31663  icoreunrn  32383  icoreelrn  32385  poimirlem3  32582  poimirlem16  32595  poimirlem17  32596  poimirlem19  32598  poimirlem30  32609  dvasin  32666  cover2  32678  upixp  32694  sdclem1  32709  fdc  32711  caushft  32727  ismtyres  32777  rrncmslem  32801  isfld2  32974  osumcllem10N  34269  pexmidlem7N  34280  dihglblem2N  35601  lcfrvalsnN  35848  lcfrlem5  35853  lcfrlem6  35854  lcfrlem27  35876  lcfrlem37  35886  monotuz  36524  expdiophlem1  36606  kelac2  36653  dvgrat  37533  nzss  37538  uzmptshftfval  37567  binomcxplemnotnn0  37577  refsumcn  38212  rfcnpre2  38213  rfcnpre3  38215  rfcnpre4  38216  elabrexg  38229  disjf1o  38373  unirnmap  38395  unirnmapsn  38401  ssmapsn  38403  allbutfi  38557  ressiocsup  38628  ressioosup  38629  ressiooinf  38631  fsumsermpt  38646  climexp  38672  climinf  38673  climsuse  38675  sumnnodd  38697  cncfiooicclem1  38779  dvsinax  38801  itgsinexplem1  38845  fvvolioof  38882  fvvolicof  38884  stoweidlem14  38907  stoweidlem16  38909  stoweidlem31  38924  stoweidlem34  38927  stoweidlem36  38929  stoweidlem43  38936  stoweidlem46  38939  stoweidlem47  38940  stoweidlem52  38945  stoweidlem55  38948  stoweidlem57  38950  dirkercncf  39000  fourierdlem20  39020  fourierdlem42  39042  fourierdlem48  39047  fourierdlem49  39048  fourierdlem51  39050  fourierdlem54  39053  fourierdlem62  39061  fourierdlem71  39070  fourierdlem80  39079  fourierdlem114  39113  fouriersw  39124  ioorrnopnlem  39200  ioorrnopnxrlem  39202  salexct3  39236  salgencntex  39237  salgensscntex  39238  subsalsal  39253  sge0fodjrnlem  39309  sge0isum  39320  sge0seq  39339  sge0reuz  39340  sge0reuzb  39341  meadjiunlem  39358  meaiininclem  39376  carageniuncllem1  39411  caratheodorylem1  39416  hoiprodp1  39478  hoidmv1lelem1  39481  hoidmv1lelem2  39482  hoidmv1le  39484  hoidmvlelem1  39485  hoidmvlelem2  39486  hoidmvlelem3  39487  voncmpl  39511  hoiqssbl  39515  smflimlem2  39658  afvres  39901  iccpartigtl  39961  ushgredgedgaloop  40458  nbgrel  40564  uvtxupgrres  40635  cplgr3v  40657  umgr2v2evd2  40743  1wlk1walk  40843  1wlkres  40879  crctcsh1wlkn0lem6  41018  wlknwwlksnfun  41085  wwlks2onv  41158  funcringcsetcALTV2lem3  41830  funcringcsetclem3ALTV  41853  lindslinindsimp2lem5  42045  onsetreclem3  42249  amgmwlem  42357