Theorem syl6eleqr 2917

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 2834	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	syl6eleq 2916	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1656   ∈ wcel 2164

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1879  df-cleq 2818  df-clel 2821

This theorem is referenced by:  3eltr4g  2923  tpnzd  4534  brelrng  5592  elabrex  6761  fliftel1  6820  ovidig  7043  unielxp  7471  tfrlem11  7755  rdglim  7793  seqomlem4  7819  2oconcl  7855  ecopqsi  8074  erov  8115  eroprf  8116  sbthlem2  8346  dffi3  8612  ixpiunwdom  8772  cantnfcl  8848  r1lim  8919  rankwflemb  8940  pwwf  8954  unwf  8957  rankwflem  8962  uniwf  8966  rankpwi  8970  rankr1g  8979  r1pw  8992  r1rankid  9006  rankuni  9010  djulcl  9056  djurcl  9057  inlresf  9060  inrresf  9062  djuun  9072  cardlim  9118  infxpenlem  9156  alephfp  9251  cfsmolem  9414  alephsing  9420  hsmexlem4  9573  axdc3lem2  9595  numth3  9614  iunfo  9683  konigthlem  9712  iunctb  9718  canthwelem  9794  canthwe  9795  r1limwun  9880  inar1  9919  inatsk  9922  gruina  9962  grur1  9964  tskmval  9983  tskmcl  9985  pinq  10071  dmrecnq  10112  addclsr  10227  mulclsr  10228  axaddf  10289  axmulf  10290  peano2nn  11371  uztrn2  11993  eluz2nn  12015  peano2uzs  12031  uzsupss  12070  uzsup  12964  uzrdgfni  13059  uzrdgsuci  13061  fsuppmapnn0fiub  13092  seqf  13123  ser0  13154  bcm1k  13402  bcp1nk  13404  bcpasc  13408  hashprdifel  13482  fz1isolem  13541  pr2pwpr  13557  ccatrn  13656  ccats1val2  13694  swrdccatin12lem3  13837  rexuzre  14476  limsupgre  14596  climconst  14658  rlimclim1  14660  climrlim2  14662  clim2ser  14769  clim2ser2  14770  iserex  14771  isermulc2  14772  iserle  14774  isercolllem3  14781  isercoll2  14783  climsup  14784  iseraltlem2  14797  iseraltlem3  14798  zsum  14833  isumclim3  14872  isumadd  14880  fsump1i  14882  iserabs  14928  cvgcmp  14929  cvgcmpub  14930  cvgcmpce  14931  abscvgcvg  14932  isumshft  14952  isumsplit  14953  isum1p  14954  isumrpcl  14956  isumsup2  14959  climcndslem1  14962  cvgrat  14995  clim2prod  15000  clim2div  15001  prodf1  15003  ntrivcvgn0  15010  ntrivcvgtail  15012  fprodntriv  15052  fprodabs  15084  fprodeq0  15085  iprodclim3  15110  iprodmul  15113  ef0lem  15188  fprodefsum  15204  rpnnen2lem3  15326  dvdsflip  15423  fzo0dvdseq  15429  bitsinv1  15544  smupval  15590  smueqlem  15592  seq1st  15664  algr0  15665  prmind2  15777  crth  15861  eulerthlem2  15865  prmdiv  15868  pockthlem  15987  pockthg  15988  unbenlem  15990  prmunb  15996  prmgaplem7  16139  strfv2d  16275  imasvscaval  16558  oppccatid  16738  epii  16762  fthepi  16947  funcestrcsetclem3  17142  funcsetcestrclem3  17156  yon12  17265  yon2  17266  yonedalem4c  17277  yonedalem22  17278  yonedalem3b  17279  yonedainv  17281  acsmapd  17538  mgm2nsgrplem1  17766  mgm2nsgrplem2  17767  mgm2nsgrplem3  17768  sgrp2nmndlem1  17771  sgrp2rid2  17774  cntrsubgnsg  18130  pmtrrn  18234  gexcl3  18360  efgi  18490  efgi2  18496  efgs1b  18507  efgredlemg  18514  efgredlemd  18516  frgpnabllem1  18636  cycsubgcyg  18662  gsumzaddlem  18681  dprdwd  18771  dprd2da  18802  lsppratlem3  19517  lsppratlem4  19518  lbsextlem2  19527  lidl0  19587  lidl1  19588  mplsubrglem  19807  mpfconst  19897  mpfproj  19898  mpfind  19903  pf1const  20077  pf1id  20078  mpfpf1  20082  pf1mpf  20083  domnchr  20247  znf1o  20266  madetsumid  20642  slesolex  20864  pmatcoe1fsupp  20883  mat2pmatbas0  20909  pmatcollpw  20963  pm2mpf1  20981  isclo  21269  indiscld  21273  restntr  21364  ordtbaslem  21370  ordtbas2  21373  lmconst  21443  lmss  21480  conncompid  21612  2ndcomap  21639  locfincmp  21707  comppfsc  21713  xkouni  21780  txcls  21785  ptclsg  21796  uptx  21806  txindis  21815  tx1stc  21831  cnmpt1res  21857  tgqtop  21893  uffix  22102  cnpflf2  22181  ptcmplem2  22234  ptcmplem4  22236  tgpconncomp  22293  tsmsfbas  22308  fmucnd  22473  prdsxmetlem  22550  imasdsf1olem  22555  prdsbl  22673  blcvx  22978  xrsmopn  22992  xrge0tsms  23014  metdcn2  23019  expcncf  23102  cnmpt2pc  23104  icchmeo  23117  iccpnfhmeo  23121  cnheibor  23131  evth  23135  evth2  23136  lebnumlem2  23138  lebnumii  23142  reparphti  23173  cfilfcls  23449  minveclem2  23601  minveclem3  23604  minveclem4  23607  ovoliunlem1  23675  ovolicc1  23689  iundisj  23721  volsup  23729  uniioombllem3  23758  vitalilem2  23782  vitalilem3  23783  mbfsup  23837  mbfinf  23838  mbflimsup  23839  itg2monolem1  23923  limcflflem  24050  limccnp  24061  limccnp2  24062  dvidlem  24085  dvn2bss  24099  cpnres  24106  dvcobr  24115  dvrec  24124  c1liplem1  24165  dvcnvrelem2  24187  dvfsumrlimf  24194  dvfsumlem1  24195  dvfsumlem2  24196  dvfsumlem3  24197  dvfsumlem4  24198  dvfsumrlim  24200  dvfsum2  24203  coeeulem  24386  coeid3  24402  plycn  24423  dvntaylp  24531  taylthlem1  24533  taylthlem2  24534  ulm2  24545  ulmshftlem  24549  ulmshft  24550  ulm0  24551  ulmcn  24559  ulmdvlem3  24562  ulmdv  24563  mtest  24564  mtestbdd  24565  dvradcnv  24581  psercn2  24583  psercn  24586  pserdv  24589  abelth  24601  efif1olem2  24696  efif1olem4  24698  efifo  24700  eff1olem  24701  logcn  24799  dvloglem  24800  cxpcn3  24898  resqrtcn  24899  sqrtcn  24900  logbleb  24930  logblt  24931  asinneg  25033  atanlogsub  25063  atanbnd  25073  ressatans  25081  leibpilem2  25088  xrlimcnp  25115  efrlim  25116  scvxcvx  25132  ppiub  25349  chtub  25357  logexprlim  25370  lgseisenlem1  25520  rplogsumlem1  25593  rplogsumlem2  25594  dchrisumlem2  25599  dchrisum0flb  25619  logdivbnd  25665  pntlem3  25718  tgcgr4  25850  ltgov  25916  f1otrg  26177  eengtrkg  26292  iedgedg  26355  ushgredgedgloop  26534  ushgredgedgloopOLD  26535  subgruhgredgd  26588  uvtxupgrres  26713  cplgr3v  26740  umgr2v2evd2  26832  edginwlk  26939  wlk1walk  26943  wlkresOLD  26978  crctcshwlkn0lem6  27121  wlkiswwlks1  27173  wlknwwlksnfunOLD  27195  minvecolem1  28281  minvecolem2  28282  minvecolem4  28287  htthlem  28325  5oalem2  29065  3oalem2  29073  iundisjf  29945  fmptco1f1o  29979  xppreima  29994  xppreima2  29995  dfcnv2  30020  xrge0tsmsd  30326  rhmopp  30360  pmtrto1cl  30390  psgnfzto1stlem  30391  fzto1stfv1  30392  fzto1st  30394  fzto1stinvn  30395  psgnfzto1st  30396  smatlem  30404  smatcl  30409  tpr2rico  30499  xrmulc1cn  30517  xrge0mulc1cn  30528  esumpfinvallem  30677  ldgenpisyslem1  30767  dynkin  30771  brfae  30852  sxbrsigalem3  30875  dya2icoseg2  30881  omsmeas  30926  sibfof  30943  sseqmw  30995  sseqf  30996  sseqp1  30999  fiblem  31002  fibp1  31005  probfinmeasbOLD  31032  repr0  31234  reprpmtf1o  31249  hgt750lemg  31277  bnj1379  31443  subfacp1lem5  31708  subfacp1lem6  31709  cvxpconn  31766  cvxsconn  31767  cvmliftlem6  31814  cvmliftlem8  31816  cvmliftlem10  31818  cvmlift2lem6  31832  cvmlift2lem11  31837  cvmlift2lem12  31838  msubff  31969  msubco  31970  elmsta  31987  msubff1  31995  mvhf  31997  msubvrs  31999  iprodefisumlem  32164  filnetlem3  32908  knoppcnlem10  33020  knoppcnlem11  33021  icoreunrn  33751  icoreelrn  33753  poimirlem3  33955  poimirlem16  33968  poimirlem17  33969  poimirlem19  33971  poimirlem30  33982  dvasin  34038  cover2  34050  upixp  34066  sdclem1  34080  fdc  34082  caushft  34098  ismtyres  34148  rrncmslem  34172  isfld2  34345  osumcllem10N  36039  pexmidlem7N  36050  dihglblem2N  37368  lcfrvalsnN  37615  lcfrlem5  37620  lcfrlem6  37621  lcfrlem27  37643  lcfrlem37  37653  monotuz  38348  expdiophlem1  38430  kelac2  38477  dvgrat  39350  nzss  39355  uzmptshftfval  39384  binomcxplemnotnn0  39394  refsumcn  40006  rfcnpre2  40007  rfcnpre3  40009  rfcnpre4  40010  elabrexg  40023  disjf1o  40185  unirnmap  40205  unirnmapsn  40211  ssmapsn  40213  mptssid  40249  allbutfi  40409  eluzd  40428  uzidd2  40436  ressiocsup  40574  ressioosup  40575  ressiooinf  40577  fsumsermpt  40604  climexp  40630  climinf  40631  climsuse  40633  sumnnodd  40655  limsupresico  40725  limsupubuzlem  40737  limsupresxr  40791  liminfresxr  40792  liminfresico  40796  limsup10exlem  40797  cnrefiisplem  40848  cncfiooicclem1  40899  dvsinax  40920  itgsinexplem1  40962  fvvolioof  40998  fvvolicof  41000  stoweidlem14  41023  stoweidlem16  41025  stoweidlem31  41040  stoweidlem34  41043  stoweidlem36  41045  stoweidlem43  41052  stoweidlem46  41055  stoweidlem47  41056  stoweidlem52  41061  stoweidlem55  41064  stoweidlem57  41066  dirkercncf  41116  fourierdlem20  41136  fourierdlem42  41158  fourierdlem48  41163  fourierdlem49  41164  fourierdlem51  41166  fourierdlem54  41169  fourierdlem62  41177  fourierdlem71  41186  fourierdlem80  41195  fourierdlem114  41229  fouriersw  41240  ioorrnopnlem  41313  ioorrnopnxrlem  41315  salexct3  41349  salgencntex  41350  salgensscntex  41351  subsalsal  41366  sge0fodjrnlem  41422  sge0isum  41433  sge0seq  41452  sge0reuz  41453  sge0reuzb  41454  meadjiunlem  41471  meaiininclem  41492  carageniuncllem1  41527  caratheodorylem1  41532  hoiprodp1  41594  hoidmv1lelem1  41597  hoidmv1lelem2  41598  hoidmv1le  41600  hoidmvlelem1  41601  hoidmvlelem2  41602  hoidmvlelem3  41603  voncmpl  41627  hoiqssbl  41631  smflimlem2  41772  smfsuplem1  41809  smfsuplem3  41811  afvres  42072  afv2res  42139  iccpartigtl  42245  prproropf1olem2  42270  ushrisomgr  42577  sprsymrelf  42610  funcringcsetcALTV2lem3  42903  funcringcsetclem3ALTV  42926  lindslinindsimp2lem5  43116  rrxsphere  43314  line2  43318  onsetreclem3  43362  amgmwlem  43458