MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl6eleqr Structured version   Visualization version   GIF version

Theorem syl6eleqr 2895
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
StepHypRef Expression
1 syl6eleqr.1 . 2 (𝜑𝐴𝐵)
2 syl6eleqr.2 . . 3 𝐶 = 𝐵
32eqcomi 2814 . 2 𝐵 = 𝐶
41, 3syl6eleq 2894 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  wcel 2158
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-9 2167  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2798  df-clel 2801
This theorem is referenced by:  3eltr4g  2901  tpnzd  4500  brelrng  5553  elabrex  6722  fliftel1  6781  ovidig  7005  unielxp  7433  tfrlem11  7717  rdglim  7755  seqomlem4  7781  2oconcl  7817  ecopqsi  8036  erov  8077  eroprf  8078  sbthlem2  8307  dffi3  8573  ixpiunwdom  8732  cantnfcl  8808  r1lim  8879  rankwflemb  8900  pwwf  8914  unwf  8917  rankwflem  8922  uniwf  8926  rankpwi  8930  rankr1g  8939  r1pw  8952  r1rankid  8966  rankuni  8970  djulcl  9016  djurcl  9017  inlresf  9020  inrresf  9022  djuun  9032  cardlim  9078  infxpenlem  9116  alephfp  9211  cfsmolem  9374  alephsing  9380  hsmexlem4  9533  axdc3lem2  9555  numth3  9574  iunfo  9643  konigthlem  9672  iunctb  9678  canthwelem  9754  canthwe  9755  r1limwun  9840  inar1  9879  inatsk  9882  gruina  9922  grur1  9924  tskmval  9943  tskmcl  9945  pinq  10031  dmrecnq  10072  addclsr  10186  mulclsr  10187  axaddf  10248  axmulf  10249  peano2nn  11314  uztrn2  11918  eluz2nn  11940  peano2uzs  11956  uzsupss  11995  uzsup  12882  uzrdgfni  12977  uzrdgsuci  12979  fsuppmapnn0fiub  13010  seqf  13041  ser0  13072  bcm1k  13318  bcp1nk  13320  bcpasc  13324  hashprdifel  13399  fz1isolem  13458  pr2pwpr  13474  ccatrn  13582  ccats1val2  13621  swrdccatin12lem3  13710  rexuzre  14311  limsupgre  14431  climconst  14493  rlimclim1  14495  climrlim2  14497  clim2ser  14604  clim2ser2  14605  iserex  14606  isermulc2  14607  iserle  14609  isercolllem3  14616  isercoll2  14618  climsup  14619  iseraltlem2  14632  iseraltlem3  14633  zsum  14668  isumclim3  14709  isumadd  14717  fsump1i  14719  iserabs  14765  cvgcmp  14766  cvgcmpub  14767  cvgcmpce  14768  abscvgcvg  14769  isumshft  14789  isumsplit  14790  isum1p  14791  isumrpcl  14793  isumsup2  14796  climcndslem1  14799  cvgrat  14832  clim2prod  14837  clim2div  14838  prodf1  14840  ntrivcvgn0  14847  ntrivcvgtail  14849  fprodntriv  14889  fprodabs  14921  fprodeq0  14922  iprodclim3  14947  iprodmul  14950  ef0lem  15025  fprodefsum  15041  rpnnen2lem3  15161  dvdsflip  15258  fzo0dvdseq  15264  bitsinv1  15379  smupval  15425  smueqlem  15427  seq1st  15499  algr0  15500  prmind2  15612  crth  15696  eulerthlem2  15700  prmdiv  15703  pockthlem  15822  pockthg  15823  unbenlem  15825  prmunb  15831  prmgaplem7  15974  strfv2d  16112  imasvscaval  16399  oppccatid  16579  epii  16603  fthepi  16788  funcestrcsetclem3  16983  funcsetcestrclem3  16997  yon12  17106  yon2  17107  yonedalem4c  17118  yonedalem22  17119  yonedalem3b  17120  yonedainv  17122  acsmapd  17379  mgm2nsgrplem1  17606  mgm2nsgrplem2  17607  mgm2nsgrplem3  17608  sgrp2nmndlem1  17611  sgrp2rid2  17614  cntrsubgnsg  17970  pmtrrn  18074  gexcl3  18199  efgi  18329  efgi2  18335  efgs1b  18346  efgredlemg  18352  efgredlemd  18354  frgpnabllem1  18473  cycsubgcyg  18499  gsumzaddlem  18518  dprdwd  18608  dprd2da  18639  lsppratlem3  19354  lsppratlem4  19355  lbsextlem2  19364  lidl0  19424  lidl1  19425  mplsubrglem  19644  mpfconst  19734  mpfproj  19735  mpfind  19740  pf1const  19914  pf1id  19915  mpfpf1  19919  pf1mpf  19920  domnchr  20084  znf1o  20103  madetsumid  20474  slesolex  20696  pmatcoe1fsupp  20715  mat2pmatbas0  20741  pmatcollpw  20795  pm2mpf1  20813  isclo  21101  indiscld  21105  restntr  21196  ordtbaslem  21202  ordtbas2  21205  lmconst  21275  lmss  21312  conncompid  21444  2ndcomap  21471  locfincmp  21539  comppfsc  21545  xkouni  21612  txcls  21617  ptclsg  21628  uptx  21638  txindis  21647  tx1stc  21663  cnmpt1res  21689  tgqtop  21725  uffix  21934  cnpflf2  22013  ptcmplem2  22066  ptcmplem4  22068  tgpconncomp  22125  tsmsfbas  22140  fmucnd  22305  prdsxmetlem  22382  imasdsf1olem  22387  prdsbl  22505  blcvx  22810  xrsmopn  22824  xrge0tsms  22846  metdcn2  22851  expcncf  22934  cnmpt2pc  22936  icchmeo  22949  iccpnfhmeo  22953  cnheibor  22963  evth  22967  evth2  22968  lebnumlem2  22970  lebnumii  22974  reparphti  23005  cfilfcls  23280  minveclem2  23405  minveclem3  23408  minveclem4  23411  ovoliunlem1  23479  ovolicc1  23493  iundisj  23525  volsup  23533  uniioombllem3  23562  vitalilem2  23586  vitalilem3  23587  mbfsup  23641  mbfinf  23642  mbflimsup  23643  itg2monolem1  23727  limcflflem  23854  limccnp  23865  limccnp2  23866  dvidlem  23889  dvn2bss  23903  cpnres  23910  dvcobr  23919  dvrec  23928  c1liplem1  23969  dvcnvrelem2  23991  dvfsumrlimf  23998  dvfsumlem1  23999  dvfsumlem2  24000  dvfsumlem3  24001  dvfsumlem4  24002  dvfsumrlim  24004  dvfsum2  24007  coeeulem  24190  coeid3  24206  plycn  24227  dvntaylp  24335  taylthlem1  24337  taylthlem2  24338  ulm2  24349  ulmshftlem  24353  ulmshft  24354  ulm0  24355  ulmcn  24363  ulmdvlem3  24366  ulmdv  24367  mtest  24368  mtestbdd  24369  dvradcnv  24385  psercn2  24387  psercn  24390  pserdv  24393  abelth  24405  efif1olem2  24500  efif1olem4  24502  efifo  24504  eff1olem  24505  logcn  24603  dvloglem  24604  cxpcn3  24699  resqrtcn  24700  sqrtcn  24701  logbleb  24731  logblt  24732  asinneg  24823  atanlogsub  24853  atanbnd  24863  ressatans  24871  leibpilem2  24878  xrlimcnp  24905  efrlim  24906  scvxcvx  24922  ppiub  25139  chtub  25147  logexprlim  25160  lgseisenlem1  25310  rplogsumlem1  25383  rplogsumlem2  25384  dchrisumlem2  25389  dchrisum0flb  25409  logdivbnd  25455  pntlem3  25508  tgcgr4  25636  ltgov  25702  f1otrg  25961  eengtrkg  26075  iedgedg  26153  ushgredgedgloop  26334  ushgredgedgloopOLD  26335  subgruhgredgd  26388  nbgrelOLD  26446  uvtxupgrres  26527  cplgr3v  26555  umgr2v2evd2  26647  edginwlk  26754  wlk1walk  26759  wlkres  26791  crctcshwlkn0lem6  26932  wlkiswwlks1  26990  wlknwwlksnfunOLD  27011  minvecolem1  28055  minvecolem2  28056  minvecolem4  28061  htthlem  28099  5oalem2  28839  3oalem2  28847  iundisjf  29724  fmptco1f1o  29758  xppreima  29773  xppreima2  29774  dfcnv2  29800  xrge0tsmsd  30107  rhmopp  30141  pmtrto1cl  30171  psgnfzto1stlem  30172  fzto1stfv1  30173  fzto1st  30175  fzto1stinvn  30176  psgnfzto1st  30177  smatlem  30185  smatcl  30190  tpr2rico  30280  xrmulc1cn  30298  xrge0mulc1cn  30309  esumpfinvallem  30458  ldgenpisyslem1  30548  dynkin  30552  brfae  30633  sxbrsigalem3  30656  dya2icoseg2  30662  omsmeas  30707  sibfof  30724  sseqmw  30775  sseqf  30776  sseqp1  30779  fiblem  30782  fibp1  30785  probfinmeasbOLD  30812  repr0  31011  reprpmtf1o  31026  hgt750lemg  31054  bnj1379  31221  subfacp1lem5  31486  subfacp1lem6  31487  cvxpconn  31544  cvxsconn  31545  cvmliftlem6  31592  cvmliftlem8  31594  cvmliftlem10  31596  cvmlift2lem6  31610  cvmlift2lem11  31615  cvmlift2lem12  31616  msubff  31747  msubco  31748  elmsta  31765  msubff1  31773  mvhf  31775  msubvrs  31777  iprodefisumlem  31945  filnetlem3  32693  knoppcnlem10  32806  knoppcnlem11  32807  icoreunrn  33520  icoreelrn  33522  poimirlem3  33722  poimirlem16  33735  poimirlem17  33736  poimirlem19  33738  poimirlem30  33749  dvasin  33805  cover2  33817  upixp  33833  sdclem1  33847  fdc  33849  caushft  33865  ismtyres  33915  rrncmslem  33939  isfld2  34112  osumcllem10N  35742  pexmidlem7N  35753  dihglblem2N  37072  lcfrvalsnN  37319  lcfrlem5  37324  lcfrlem6  37325  lcfrlem27  37347  lcfrlem37  37357  monotuz  38004  expdiophlem1  38086  kelac2  38133  dvgrat  39008  nzss  39013  uzmptshftfval  39042  binomcxplemnotnn0  39052  refsumcn  39680  rfcnpre2  39681  rfcnpre3  39683  rfcnpre4  39684  elabrexg  39697  disjf1o  39864  unirnmap  39884  unirnmapsn  39890  ssmapsn  39892  mptssid  39931  allbutfi  40092  eluzd  40111  uzidd2  40119  ressiocsup  40258  ressioosup  40259  ressiooinf  40261  fsumsermpt  40288  climexp  40314  climinf  40315  climsuse  40317  sumnnodd  40339  limsupresico  40409  limsupubuzlem  40421  limsupresxr  40475  liminfresxr  40476  liminfresico  40480  limsup10exlem  40481  cnrefiisplem  40532  cncfiooicclem1  40583  dvsinax  40604  itgsinexplem1  40646  fvvolioof  40682  fvvolicof  40684  stoweidlem14  40707  stoweidlem16  40709  stoweidlem31  40724  stoweidlem34  40727  stoweidlem36  40729  stoweidlem43  40736  stoweidlem46  40739  stoweidlem47  40740  stoweidlem52  40745  stoweidlem55  40748  stoweidlem57  40750  dirkercncf  40800  fourierdlem20  40820  fourierdlem42  40842  fourierdlem48  40847  fourierdlem49  40848  fourierdlem51  40850  fourierdlem54  40853  fourierdlem62  40861  fourierdlem71  40870  fourierdlem80  40879  fourierdlem114  40913  fouriersw  40924  ioorrnopnlem  41000  ioorrnopnxrlem  41002  salexct3  41036  salgencntex  41037  salgensscntex  41038  subsalsal  41053  sge0fodjrnlem  41109  sge0isum  41120  sge0seq  41139  sge0reuz  41140  sge0reuzb  41141  meadjiunlem  41158  meaiininclem  41179  carageniuncllem1  41214  caratheodorylem1  41219  hoiprodp1  41281  hoidmv1lelem1  41284  hoidmv1lelem2  41285  hoidmv1le  41287  hoidmvlelem1  41288  hoidmvlelem2  41289  hoidmvlelem3  41290  voncmpl  41314  hoiqssbl  41318  smflimlem2  41459  smfsuplem1  41496  smfsuplem3  41498  afvres  41758  afv2res  41825  iccpartigtl  41931  sprsymrelf  42310  funcringcsetcALTV2lem3  42603  funcringcsetclem3ALTV  42626  lindslinindsimp2lem5  42816  onsetreclem3  43018  amgmwlem  43116
  Copyright terms: Public domain W3C validator