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

Theorem syl6eleqr 2695
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 2615 . 2 𝐵 = 𝐶
41, 3syl6eleq 2694 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wcel 1976
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-cleq 2599  df-clel 2602
This theorem is referenced by:  3eltr4g  2701  tpnzd  4253  brelrng  5260  elabrex  6380  fliftel1  6435  ovidig  6651  unielxp  7069  tfrlem11  7345  rdglim  7383  seqomlem4  7409  2oconcl  7444  ecopqsi  7665  erov  7705  eroprf  7706  sbthlem2  7930  dffi3  8194  ixpiunwdom  8353  cantnfcl  8421  r1lim  8492  rankwflemb  8513  pwwf  8527  unwf  8530  rankwflem  8535  uniwf  8539  rankpwi  8543  rankr1g  8552  r1pw  8565  r1rankid  8579  rankuni  8583  cardlim  8655  infxpenlem  8693  alephfp  8788  cfsmolem  8949  alephsing  8955  hsmexlem4  9108  axdc3lem2  9130  numth3  9149  iunfo  9214  konigthlem  9243  iunctb  9249  canthwelem  9325  canthwe  9326  r1limwun  9411  inar1  9450  inatsk  9453  gruina  9493  grur1  9495  tskmval  9514  tskmcl  9516  pinq  9602  dmrecnq  9643  addclsr  9757  mulclsr  9758  axaddf  9819  axmulf  9820  peano2nn  10876  uztrn2  11534  eluz2nn  11555  peano2uzs  11571  uzsupss  11609  uzsup  12476  uzrdgfni  12571  uzrdgsuci  12573  fsuppmapnn0fiub  12604  seqf  12636  ser0  12667  bcm1k  12916  bcp1nk  12918  bcpasc  12922  hashprdifel  12996  fz1isolem  13051  pr2pwpr  13063  ccatrn  13168  ccats1val2  13199  swrdccatin12lem3  13284  rexuzre  13883  limsupgre  14003  climconst  14065  rlimclim1  14067  climrlim2  14069  clim2ser  14176  clim2ser2  14177  iserex  14178  isermulc2  14179  iserle  14181  isercolllem3  14188  isercoll2  14190  climsup  14191  iseraltlem2  14204  iseraltlem3  14205  zsum  14239  isumclim3  14275  isumadd  14283  fsump1i  14285  iserabs  14331  cvgcmp  14332  cvgcmpub  14333  cvgcmpce  14334  abscvgcvg  14335  isumshft  14353  isumsplit  14354  isum1p  14355  isumrpcl  14357  isumsup2  14360  climcndslem1  14363  cvgrat  14397  clim2prod  14402  clim2div  14403  prodf1  14405  ntrivcvgn0  14412  ntrivcvgtail  14414  fprodntriv  14454  fprodabs  14486  fprodeq0  14487  iprodclim3  14513  iprodmul  14516  ef0lem  14591  fprodefsum  14607  rpnnen2lem3  14727  dvdsflip  14820  fzo0dvdseq  14826  bitsinv1  14945  smupval  14991  smueqlem  14993  seq1st  15065  algr0  15066  prmind2  15179  crth  15264  eulerthlem2  15268  prmdiv  15271  pockthlem  15390  pockthg  15391  unbenlem  15393  prmunb  15399  prmgaplem7  15542  strfv2d  15676  imasvscaval  15964  oppccatid  16145  epii  16169  fthepi  16354  funcestrcsetclem3  16548  funcsetcestrclem3  16562  yon12  16671  yon2  16672  yonedalem4c  16683  yonedalem22  16684  yonedalem3b  16685  yonedainv  16687  acsmapd  16944  mgm2nsgrplem1  17171  mgm2nsgrplem2  17172  mgm2nsgrplem3  17173  sgrp2nmndlem1  17176  sgrp2rid2  17179  cntrsubgnsg  17539  pmtrrn  17643  gexcl3  17768  efgi  17898  efgi2  17904  efgs1b  17915  efgredlemg  17921  efgredlemd  17923  frgpnabllem1  18042  cycsubgcyg  18068  gsumzaddlem  18087  dprdwd  18176  dprd2da  18207  lsppratlem3  18913  lsppratlem4  18914  lbsextlem2  18923  lidl0  18983  lidl1  18984  mplsubrglem  19203  mpfconst  19294  mpfproj  19295  mpfind  19300  pf1const  19474  pf1id  19475  mpfpf1  19479  pf1mpf  19480  domnchr  19641  znf1o  19661  madetsumid  20025  slesolex  20246  pmatcoe1fsupp  20264  mat2pmatbas0  20290  pmatcollpw  20344  pm2mpf1  20362  isclo  20640  indiscld  20644  restntr  20735  ordtbaslem  20741  ordtbas2  20744  lmconst  20814  lmss  20851  concompid  20983  2ndcomap  21010  locfincmp  21078  comppfsc  21084  xkouni  21151  txcls  21156  ptclsg  21167  uptx  21177  txindis  21186  tx1stc  21202  cnmpt1res  21228  tgqtop  21264  uffix  21474  cnpflf2  21553  ptcmplem2  21606  ptcmplem4  21608  tgpconcomp  21665  tsmsfbas  21680  fmucnd  21845  prdsxmetlem  21921  imasdsf1olem  21926  prdsbl  22044  blcvx  22338  xrsmopn  22352  xrge0tsms  22374  metdcn2  22379  expcncf  22461  cnmpt2pc  22463  icchmeo  22476  iccpnfhmeo  22480  cnheibor  22490  evth  22494  evth2  22495  lebnumlem2  22497  lebnumii  22501  reparphti  22533  cfilfcls  22795  minveclem2  22919  minveclem3  22922  minveclem4  22925  ovoliunlem1  22991  ovolicc1  23005  iundisj  23037  volsup  23045  uniioombllem3  23073  vitalilem2  23098  vitalilem3  23099  mbfsup  23151  mbfinf  23152  mbflimsup  23153  itg2monolem1  23237  limcflflem  23364  limccnp  23375  limccnp2  23376  dvidlem  23399  dvn2bss  23413  cpnres  23420  dvcobr  23429  dvrec  23438  c1liplem1  23477  dvcnvrelem2  23499  dvfsumrlimf  23506  dvfsumlem1  23507  dvfsumlem2  23508  dvfsumlem3  23509  dvfsumlem4  23510  dvfsumrlim  23512  dvfsum2  23515  coeeulem  23698  coeid3  23714  plycn  23735  dvntaylp  23843  taylthlem1  23845  taylthlem2  23846  ulm2  23857  ulmshftlem  23861  ulmshft  23862  ulm0  23863  ulmcn  23871  ulmdvlem3  23874  ulmdv  23875  mtest  23876  mtestbdd  23877  dvradcnv  23893  psercn2  23895  psercn  23898  pserdv  23901  abelth  23913  efif1olem2  24007  efif1olem4  24009  efifo  24011  eff1olem  24012  logcn  24107  dvloglem  24108  cxpcn3  24203  resqrtcn  24204  sqrtcn  24205  logbleb  24235  logblt  24236  asinneg  24327  atanlogsub  24357  atanbnd  24367  ressatans  24375  leibpilem2  24382  xrlimcnp  24409  efrlim  24410  scvxcvx  24426  ppiub  24643  chtub  24651  logexprlim  24664  lgseisenlem1  24814  rplogsumlem1  24887  rplogsumlem2  24888  dchrisumlem2  24893  dchrisum0flb  24913  logdivbnd  24959  pntlem3  25012  tgcgr4  25141  ltgov  25207  f1otrg  25466  eengtrkg  25580  nbgraf1olem3  25735  cusgrares  25764  wlknwwlknfun  26001  eupap1  26266  minvecolem1  26917  minvecolem2  26918  minvecolem4  26923  htthlem  26961  5oalem2  27701  3oalem2  27709  iundisjf  28587  xppreima  28632  xppreima2  28633  dfcnv2  28662  xrge0tsmsd  28919  rhmopp  28953  pmtrto1cl  28983  psgnfzto1stlem  28984  fzto1stfv1  28985  fzto1st  28987  fzto1stinvn  28988  psgnfzto1st  28989  smatlem  28994  smatcl  28999  tpr2rico  29089  xrmulc1cn  29107  xrge0mulc1cn  29118  esumpfinvallem  29266  ldgenpisyslem1  29356  dynkin  29360  brfae  29441  sxbrsigalem3  29464  dya2icoseg2  29470  omsmeas  29515  sibfof  29532  sseqmw  29583  sseqf  29584  sseqp1  29587  fiblem  29590  fibp1  29593  probfinmeasbOLD  29620  bnj1379  29958  subfacp1lem5  30223  subfacp1lem6  30224  cvxpcon  30281  cvxscon  30282  cvmliftlem6  30329  cvmliftlem8  30331  cvmliftlem10  30333  cvmlift2lem6  30347  cvmlift2lem11  30352  cvmlift2lem12  30353  msubff  30484  msubco  30485  elmsta  30502  msubff1  30510  mvhf  30512  msubvrs  30514  iprodefisumlem  30682  nobndlem2  30895  nobndlem6  30899  nofulllem3  30906  filnetlem3  31348  knoppcnlem10  31465  knoppcnlem11  31466  icoreunrn  32183  icoreelrn  32185  poimirlem3  32382  poimirlem16  32395  poimirlem17  32396  poimirlem19  32398  poimirlem30  32409  dvasin  32466  cover2  32478  upixp  32494  sdclem1  32509  fdc  32511  caushft  32527  ismtyres  32577  rrncmslem  32601  isfld2  32774  osumcllem10N  34069  pexmidlem7N  34080  dihglblem2N  35401  lcfrvalsnN  35648  lcfrlem5  35653  lcfrlem6  35654  lcfrlem27  35676  lcfrlem37  35686  monotuz  36324  expdiophlem1  36406  kelac2  36453  dvgrat  37333  nzss  37338  uzmptshftfval  37367  binomcxplemnotnn0  37377  refsumcn  38012  rfcnpre2  38013  rfcnpre3  38015  rfcnpre4  38016  elabrexg  38029  disjf1o  38173  unirnmap  38195  unirnmapsn  38201  ssmapsn  38203  allbutfi  38358  ressiocsup  38429  ressioosup  38430  ressiooinf  38432  fsumsermpt  38447  climexp  38473  climinf  38474  climsuse  38476  sumnnodd  38498  cncfiooicclem1  38580  dvsinax  38602  itgsinexplem1  38646  fvvolioof  38683  fvvolicof  38685  stoweidlem14  38708  stoweidlem16  38710  stoweidlem31  38725  stoweidlem34  38728  stoweidlem36  38730  stoweidlem43  38737  stoweidlem46  38740  stoweidlem47  38741  stoweidlem52  38746  stoweidlem55  38749  stoweidlem57  38751  dirkercncf  38801  fourierdlem20  38821  fourierdlem42  38843  fourierdlem48  38848  fourierdlem49  38849  fourierdlem51  38851  fourierdlem54  38854  fourierdlem62  38862  fourierdlem71  38871  fourierdlem80  38880  fourierdlem114  38914  fouriersw  38925  ioorrnopnlem  39001  ioorrnopnxrlem  39003  salexct3  39037  salgencntex  39038  salgensscntex  39039  subsalsal  39054  sge0fodjrnlem  39110  sge0isum  39121  sge0seq  39140  sge0reuz  39141  sge0reuzb  39142  meadjiunlem  39159  meaiininclem  39177  carageniuncllem1  39212  caratheodorylem1  39217  hoiprodp1  39279  hoidmv1lelem1  39282  hoidmv1lelem2  39283  hoidmv1le  39285  hoidmvlelem1  39286  hoidmvlelem2  39287  hoidmvlelem3  39288  voncmpl  39312  hoiqssbl  39316  smflimlem2  39459  afvres  39703  iccpartigtl  39763  ushgredgedgaloop  40457  nbgrel  40563  uvtxupgrres  40634  cplgr3v  40656  umgr2v2evd2  40742  1wlk1walk  40842  1wlkres  40878  crctcsh1wlkn0lem6  41017  wlknwwlksnfun  41084  wwlks2onv  41157  funcringcsetcALTV2lem3  41829  funcringcsetclem3ALTV  41852  lindslinindsimp2lem5  42044  amgmwlem  42317
  Copyright terms: Public domain W3C validator