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

Theorem syl6eleqr 2709
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 2630 . 2 𝐵 = 𝐶
41, 3syl6eleq 2708 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  wcel 1987
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-cleq 2614  df-clel 2617
This theorem is referenced by:  3eltr4g  2715  tpnzd  4291  brelrng  5325  elabrex  6466  fliftel1  6525  ovidig  6743  unielxp  7164  tfrlem11  7444  rdglim  7482  seqomlem4  7508  2oconcl  7543  ecopqsi  7764  erov  7804  eroprf  7805  sbthlem2  8031  dffi3  8297  ixpiunwdom  8456  cantnfcl  8524  r1lim  8595  rankwflemb  8616  pwwf  8630  unwf  8633  rankwflem  8638  uniwf  8642  rankpwi  8646  rankr1g  8655  r1pw  8668  r1rankid  8682  rankuni  8686  cardlim  8758  infxpenlem  8796  alephfp  8891  cfsmolem  9052  alephsing  9058  hsmexlem4  9211  axdc3lem2  9233  numth3  9252  iunfo  9321  konigthlem  9350  iunctb  9356  canthwelem  9432  canthwe  9433  r1limwun  9518  inar1  9557  inatsk  9560  gruina  9600  grur1  9602  tskmval  9621  tskmcl  9623  pinq  9709  dmrecnq  9750  addclsr  9864  mulclsr  9865  axaddf  9926  axmulf  9927  peano2nn  10992  uztrn2  11665  eluz2nn  11686  peano2uzs  11702  uzsupss  11740  uzsup  12618  uzrdgfni  12713  uzrdgsuci  12715  fsuppmapnn0fiub  12746  seqf  12778  ser0  12809  bcm1k  13058  bcp1nk  13060  bcpasc  13064  hashprdifel  13142  fz1isolem  13199  pr2pwpr  13215  ccatrn  13327  ccats1val2  13358  swrdccatin12lem3  13443  rexuzre  14042  limsupgre  14162  climconst  14224  rlimclim1  14226  climrlim2  14228  clim2ser  14335  clim2ser2  14336  iserex  14337  isermulc2  14338  iserle  14340  isercolllem3  14347  isercoll2  14349  climsup  14350  iseraltlem2  14363  iseraltlem3  14364  zsum  14398  isumclim3  14437  isumadd  14445  fsump1i  14447  iserabs  14493  cvgcmp  14494  cvgcmpub  14495  cvgcmpce  14496  abscvgcvg  14497  isumshft  14515  isumsplit  14516  isum1p  14517  isumrpcl  14519  isumsup2  14522  climcndslem1  14525  cvgrat  14559  clim2prod  14564  clim2div  14565  prodf1  14567  ntrivcvgn0  14574  ntrivcvgtail  14576  fprodntriv  14616  fprodabs  14648  fprodeq0  14649  iprodclim3  14675  iprodmul  14678  ef0lem  14753  fprodefsum  14769  rpnnen2lem3  14889  dvdsflip  14982  fzo0dvdseq  14988  bitsinv1  15107  smupval  15153  smueqlem  15155  seq1st  15227  algr0  15228  prmind2  15341  crth  15426  eulerthlem2  15430  prmdiv  15433  pockthlem  15552  pockthg  15553  unbenlem  15555  prmunb  15561  prmgaplem7  15704  strfv2d  15845  imasvscaval  16138  oppccatid  16319  epii  16343  fthepi  16528  funcestrcsetclem3  16722  funcsetcestrclem3  16736  yon12  16845  yon2  16846  yonedalem4c  16857  yonedalem22  16858  yonedalem3b  16859  yonedainv  16861  acsmapd  17118  mgm2nsgrplem1  17345  mgm2nsgrplem2  17346  mgm2nsgrplem3  17347  sgrp2nmndlem1  17350  sgrp2rid2  17353  cntrsubgnsg  17713  pmtrrn  17817  gexcl3  17942  efgi  18072  efgi2  18078  efgs1b  18089  efgredlemg  18095  efgredlemd  18097  frgpnabllem1  18216  cycsubgcyg  18242  gsumzaddlem  18261  dprdwd  18350  dprd2da  18381  lsppratlem3  19089  lsppratlem4  19090  lbsextlem2  19099  lidl0  19159  lidl1  19160  mplsubrglem  19379  mpfconst  19470  mpfproj  19471  mpfind  19476  pf1const  19650  pf1id  19651  mpfpf1  19655  pf1mpf  19656  domnchr  19820  znf1o  19840  madetsumid  20207  slesolex  20428  pmatcoe1fsupp  20446  mat2pmatbas0  20472  pmatcollpw  20526  pm2mpf1  20544  isclo  20831  indiscld  20835  restntr  20926  ordtbaslem  20932  ordtbas2  20935  lmconst  21005  lmss  21042  conncompid  21174  2ndcomap  21201  locfincmp  21269  comppfsc  21275  xkouni  21342  txcls  21347  ptclsg  21358  uptx  21368  txindis  21377  tx1stc  21393  cnmpt1res  21419  tgqtop  21455  uffix  21665  cnpflf2  21744  ptcmplem2  21797  ptcmplem4  21799  tgpconncomp  21856  tsmsfbas  21871  fmucnd  22036  prdsxmetlem  22113  imasdsf1olem  22118  prdsbl  22236  blcvx  22541  xrsmopn  22555  xrge0tsms  22577  metdcn2  22582  expcncf  22665  cnmpt2pc  22667  icchmeo  22680  iccpnfhmeo  22684  cnheibor  22694  evth  22698  evth2  22699  lebnumlem2  22701  lebnumii  22705  reparphti  22737  cfilfcls  23012  minveclem2  23137  minveclem3  23140  minveclem4  23143  ovoliunlem1  23210  ovolicc1  23224  iundisj  23256  volsup  23264  uniioombllem3  23293  vitalilem2  23318  vitalilem3  23319  mbfsup  23371  mbfinf  23372  mbflimsup  23373  itg2monolem1  23457  limcflflem  23584  limccnp  23595  limccnp2  23596  dvidlem  23619  dvn2bss  23633  cpnres  23640  dvcobr  23649  dvrec  23658  c1liplem1  23697  dvcnvrelem2  23719  dvfsumrlimf  23726  dvfsumlem1  23727  dvfsumlem2  23728  dvfsumlem3  23729  dvfsumlem4  23730  dvfsumrlim  23732  dvfsum2  23735  coeeulem  23918  coeid3  23934  plycn  23955  dvntaylp  24063  taylthlem1  24065  taylthlem2  24066  ulm2  24077  ulmshftlem  24081  ulmshft  24082  ulm0  24083  ulmcn  24091  ulmdvlem3  24094  ulmdv  24095  mtest  24096  mtestbdd  24097  dvradcnv  24113  psercn2  24115  psercn  24118  pserdv  24121  abelth  24133  efif1olem2  24227  efif1olem4  24229  efifo  24231  eff1olem  24232  logcn  24327  dvloglem  24328  cxpcn3  24423  resqrtcn  24424  sqrtcn  24425  logbleb  24455  logblt  24456  asinneg  24547  atanlogsub  24577  atanbnd  24587  ressatans  24595  leibpilem2  24602  xrlimcnp  24629  efrlim  24630  scvxcvx  24646  ppiub  24863  chtub  24871  logexprlim  24884  lgseisenlem1  25034  rplogsumlem1  25107  rplogsumlem2  25108  dchrisumlem2  25113  dchrisum0flb  25133  logdivbnd  25179  pntlem3  25232  tgcgr4  25360  ltgov  25426  f1otrg  25685  eengtrkg  25799  ushgredgedgloop  26050  nbgrel  26159  uvtxupgrres  26230  cplgr3v  26252  umgr2v2evd2  26343  wlk1walk  26438  wlkres  26470  crctcshwlkn0lem6  26610  wlknwwlksnfun  26677  wwlks2onv  26750  minvecolem1  27618  minvecolem2  27619  minvecolem4  27624  htthlem  27662  5oalem2  28402  3oalem2  28410  iundisjf  29288  xppreima  29332  xppreima2  29333  dfcnv2  29360  xrge0tsmsd  29612  rhmopp  29646  pmtrto1cl  29676  psgnfzto1stlem  29677  fzto1stfv1  29678  fzto1st  29680  fzto1stinvn  29681  psgnfzto1st  29682  smatlem  29687  smatcl  29692  tpr2rico  29782  xrmulc1cn  29800  xrge0mulc1cn  29811  esumpfinvallem  29959  ldgenpisyslem1  30049  dynkin  30053  brfae  30134  sxbrsigalem3  30157  dya2icoseg2  30163  omsmeas  30208  sibfof  30225  sseqmw  30276  sseqf  30277  sseqp1  30280  fiblem  30283  fibp1  30286  probfinmeasbOLD  30313  brepr0  30500  bnj1379  30662  subfacp1lem5  30927  subfacp1lem6  30928  cvxpconn  30985  cvxsconn  30986  cvmliftlem6  31033  cvmliftlem8  31035  cvmliftlem10  31037  cvmlift2lem6  31051  cvmlift2lem11  31056  cvmlift2lem12  31057  msubff  31188  msubco  31189  elmsta  31206  msubff1  31214  mvhf  31216  msubvrs  31218  iprodefisumlem  31387  nobndlem2  31609  nobndlem6  31613  filnetlem3  32070  knoppcnlem10  32187  knoppcnlem11  32188  icoreunrn  32878  icoreelrn  32880  poimirlem3  33083  poimirlem16  33096  poimirlem17  33097  poimirlem19  33099  poimirlem30  33110  dvasin  33167  cover2  33179  upixp  33195  sdclem1  33210  fdc  33212  caushft  33228  ismtyres  33278  rrncmslem  33302  isfld2  33475  osumcllem10N  34770  pexmidlem7N  34781  dihglblem2N  36102  lcfrvalsnN  36349  lcfrlem5  36354  lcfrlem6  36355  lcfrlem27  36377  lcfrlem37  36387  monotuz  37025  expdiophlem1  37107  kelac2  37154  dvgrat  38032  nzss  38037  uzmptshftfval  38066  binomcxplemnotnn0  38076  refsumcn  38711  rfcnpre2  38712  rfcnpre3  38714  rfcnpre4  38715  elabrexg  38728  disjf1o  38887  unirnmap  38909  unirnmapsn  38915  ssmapsn  38917  mptssid  38960  allbutfi  39115  eluzd  39134  uzidd2  39142  ressiocsup  39227  ressioosup  39228  ressiooinf  39230  fsumsermpt  39247  climexp  39273  climinf  39274  climsuse  39276  sumnnodd  39298  limsupresico  39368  limsupubuzlem  39380  cncfiooicclem1  39441  dvsinax  39463  itgsinexplem1  39506  fvvolioof  39543  fvvolicof  39545  stoweidlem14  39568  stoweidlem16  39570  stoweidlem31  39585  stoweidlem34  39588  stoweidlem36  39590  stoweidlem43  39597  stoweidlem46  39600  stoweidlem47  39601  stoweidlem52  39606  stoweidlem55  39609  stoweidlem57  39611  dirkercncf  39661  fourierdlem20  39681  fourierdlem42  39703  fourierdlem48  39708  fourierdlem49  39709  fourierdlem51  39711  fourierdlem54  39714  fourierdlem62  39722  fourierdlem71  39731  fourierdlem80  39740  fourierdlem114  39774  fouriersw  39785  ioorrnopnlem  39861  ioorrnopnxrlem  39863  salexct3  39897  salgencntex  39898  salgensscntex  39899  subsalsal  39914  sge0fodjrnlem  39970  sge0isum  39981  sge0seq  40000  sge0reuz  40001  sge0reuzb  40002  meadjiunlem  40019  meaiininclem  40037  carageniuncllem1  40072  caratheodorylem1  40077  hoiprodp1  40139  hoidmv1lelem1  40142  hoidmv1lelem2  40143  hoidmv1le  40145  hoidmvlelem1  40146  hoidmvlelem2  40147  hoidmvlelem3  40148  voncmpl  40172  hoiqssbl  40176  smflimlem2  40317  smfsuplem1  40354  smfsuplem3  40356  afvres  40586  iccpartigtl  40687  sprsymrelf  41063  funcringcsetcALTV2lem3  41356  funcringcsetclem3ALTV  41379  lindslinindsimp2lem5  41569  onsetreclem3  41773  amgmwlem  41881
  Copyright terms: Public domain W3C validator