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

Theorem syl6eleqr 2929
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 2835 . 2 𝐵 = 𝐶
41, 3syl6eleq 2928 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  wcel 2107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-cleq 2819  df-clel 2898
This theorem is referenced by:  3eltr4g  2935  brelrng  5810  elabrex  6998  fliftel1  7057  ovidig  7286  unielxp  7723  tfrlem11  8020  rdglim  8058  seqomlem4  8085  2oconcl  8124  ecopqsi  8349  erov  8389  eroprf  8390  sbthlem2  8622  dffi3  8889  ixpiunwdom  9049  cantnfcl  9124  r1lim  9195  rankwflemb  9216  pwwf  9230  unwf  9233  rankwflem  9238  uniwf  9242  rankpwi  9246  rankr1g  9255  r1pw  9268  r1rankid  9282  rankuni  9286  djulcl  9333  djurcl  9334  inlresf  9337  inrresf  9339  djuun  9349  cardlim  9395  infxpenlem  9433  alephfp  9528  cfsmolem  9686  alephsing  9692  hsmexlem4  9845  axdc3lem2  9867  numth3  9886  iunfo  9955  konigthlem  9984  iunctb  9990  canthwelem  10066  canthwe  10067  r1limwun  10152  inar1  10191  inatsk  10194  gruina  10234  grur1  10236  tskmval  10255  tskmcl  10257  pinq  10343  dmrecnq  10384  addclsr  10499  mulclsr  10500  axaddf  10561  axmulf  10562  peano2nn  11644  uztrn2  12256  eluz2nn  12278  peano2uzs  12296  uzsupss  12334  uzsup  13226  uzrdgfni  13321  uzrdgsuci  13323  fsuppmapnn0fiub  13354  seqf  13386  ser0  13417  bcm1k  13670  bcp1nk  13672  bcpasc  13676  hashprdifel  13754  fz1isolem  13814  pr2pwpr  13832  ccats1val2  13978  rexuzre  14707  limsupgre  14833  climconst  14895  rlimclim1  14897  climrlim2  14899  clim2ser  15006  clim2ser2  15007  iserex  15008  isermulc2  15009  iserle  15011  isercolllem3  15018  isercoll2  15020  climsup  15021  iseraltlem2  15034  iseraltlem3  15035  zsum  15070  isumclim3  15109  isumadd  15117  fsump1i  15119  iserabs  15165  cvgcmp  15166  cvgcmpub  15167  cvgcmpce  15168  abscvgcvg  15169  isumshft  15189  isumsplit  15190  isum1p  15191  isumrpcl  15193  isumsup2  15196  climcndslem1  15199  cvgrat  15234  clim2prod  15239  clim2div  15240  prodf1  15242  ntrivcvgn0  15249  ntrivcvgtail  15251  fprodntriv  15291  fprodabs  15323  fprodeq0  15324  iprodclim3  15349  iprodmul  15352  ef0lem  15427  fprodefsum  15443  rpnnen2lem3  15564  dvdsflip  15662  fzo0dvdseq  15668  bitsinv1  15786  smupval  15832  smueqlem  15834  seq1st  15910  algr0  15911  prmind2  16024  crth  16110  eulerthlem2  16114  prmdiv  16117  pockthlem  16236  pockthg  16237  unbenlem  16239  prmunb  16245  prmgaplem7  16388  strfv2d  16524  imasvscaval  16806  oppccatid  16984  epii  17008  fthepi  17193  funcestrcsetclem3  17387  funcsetcestrclem3  17401  yon12  17510  yon2  17511  yonedalem4c  17522  yonedalem22  17523  yonedalem3b  17524  yonedainv  17526  acsmapd  17783  mgm2nsgrplem1  18028  mgm2nsgrplem2  18029  mgm2nsgrplem3  18030  sgrp2nmndlem1  18033  sgrp2rid2  18036  cntrsubgnsg  18416  pmtrrn  18521  gexcl3  18648  efgi  18781  efgi2  18787  efgs1b  18798  efgredlemg  18804  efgredlemd  18806  frgpnabllem1  18929  cycsubgcyg  18957  gsumzaddlem  18977  dprdwd  19069  dprd2da  19100  lsppratlem3  19857  lsppratlem4  19858  lbsextlem2  19867  lidl0  19927  lidl1  19928  mplsubrglem  20154  mpfconst  20249  mpfproj  20250  mpfind  20255  pf1const  20444  pf1id  20445  mpfpf1  20449  pf1mpf  20450  domnchr  20614  znf1o  20633  madetsumid  21005  slesolex  21226  pmatcoe1fsupp  21244  mat2pmatbas0  21270  pmatcollpw  21324  pm2mpf1  21342  isclo  21630  indiscld  21634  restntr  21725  ordtbaslem  21731  ordtbas2  21734  lmconst  21804  lmss  21841  conncompid  21974  2ndcomap  22001  locfincmp  22069  comppfsc  22075  xkouni  22142  txcls  22147  ptclsg  22158  uptx  22168  txindis  22177  tx1stc  22193  cnmpt1res  22219  tgqtop  22255  uffix  22464  cnpflf2  22543  ptcmplem2  22596  ptcmplem4  22598  tgpconncomp  22655  tsmsfbas  22670  fmucnd  22835  prdsxmetlem  22912  imasdsf1olem  22917  prdsbl  23035  blcvx  23340  xrsmopn  23354  xrge0tsms  23376  metdcn2  23381  expcncf  23464  cnmpopc  23466  icchmeo  23479  iccpnfhmeo  23483  cnheibor  23493  evth  23497  evth2  23498  lebnumlem2  23500  lebnumii  23504  reparphti  23535  cfilfcls  23811  minveclem2  23963  minveclem3  23966  minveclem4  23969  ovoliunlem1  24037  ovolicc1  24051  iundisj  24083  volsup  24091  uniioombllem3  24120  vitalilem2  24144  vitalilem3  24145  mbfsup  24199  mbfinf  24200  mbflimsup  24201  itg2monolem1  24285  limcflflem  24412  limccnp  24423  limccnp2  24424  dvidlem  24447  dvn2bss  24461  cpnres  24468  dvcobr  24477  dvrec  24486  c1liplem1  24527  dvcnvrelem2  24549  dvfsumrlimf  24556  dvfsumlem1  24557  dvfsumlem2  24558  dvfsumlem3  24559  dvfsumlem4  24560  dvfsumrlim  24562  dvfsum2  24565  coeeulem  24748  coeid3  24764  plycn  24785  dvntaylp  24893  taylthlem1  24895  taylthlem2  24896  ulm2  24907  ulmshftlem  24911  ulmshft  24912  ulm0  24913  ulmcn  24921  ulmdvlem3  24924  ulmdv  24925  mtest  24926  mtestbdd  24927  dvradcnv  24943  psercn2  24945  psercn  24948  pserdv  24951  abelth  24963  efif1olem2  25059  efif1olem4  25061  efifo  25063  eff1olem  25064  logcn  25162  dvloglem  25163  cxpcn3  25261  resqrtcn  25262  sqrtcn  25263  logbleb  25293  logblt  25294  asinneg  25396  atanlogsub  25426  atanbnd  25436  ressatans  25444  leibpilem2  25452  xrlimcnp  25479  efrlim  25480  scvxcvx  25496  ppiub  25713  chtub  25721  logexprlim  25734  lgseisenlem1  25884  rplogsumlem1  25993  rplogsumlem2  25994  dchrisumlem2  25999  dchrisum0flb  26019  logdivbnd  26065  pntlem3  26118  tgcgr4  26250  ltgov  26316  f1otrg  26590  eengtrkg  26705  iedgedg  26768  ushgredgedgloop  26946  subgruhgredgd  26999  uvtxupgrres  27123  umgr2v2evd2  27242  edginwlk  27349  wlk1walk  27353  crctcshwlkn0lem6  27526  wlkiswwlks1  27578  minvecolem1  28584  minvecolem2  28585  minvecolem4  28590  htthlem  28627  5oalem2  29365  3oalem2  29373  iundisjf  30273  fmptco1f1o  30312  xppreima  30328  xppreima2  30329  dfcnv2  30356  xrge0tsmsd  30625  odpmco  30663  pmtrcnelor  30668  pmtrto1cl  30674  psgnfzto1stlem  30675  fzto1stfv1  30676  fzto1st  30678  fzto1stinvn  30679  psgnfzto1st  30680  tocycf  30692  cycpmco2lem7  30707  cycpmco2  30708  cycpmrn  30718  cyc3evpm  30725  cyc3genpmlem  30726  cycpmgcl  30728  cyc3conja  30732  rhmopp  30825  fply1  30864  smatlem  30967  smatcl  30972  tpr2rico  31060  xrmulc1cn  31078  xrge0mulc1cn  31089  esumpfinvallem  31238  ldgenpisyslem1  31327  dynkin  31331  brfae  31412  sxbrsigalem3  31435  dya2icoseg2  31441  omsmeas  31486  sibfof  31503  sseqmw  31554  sseqf  31555  sseqp1  31558  fiblem  31561  fibp1  31564  probfinmeasbALTV  31592  repr0  31787  reprpmtf1o  31802  hgt750lemg  31830  bnj1379  32007  srcmpltd  32249  subfacp1lem5  32334  subfacp1lem6  32335  cvxpconn  32392  cvxsconn  32393  cvmliftlem6  32440  cvmliftlem8  32442  cvmliftlem10  32444  cvmlift2lem6  32458  cvmlift2lem11  32463  cvmlift2lem12  32464  2goelgoanfmla1  32574  prv1n  32581  msubff  32680  msubco  32681  elmsta  32698  msubff1  32706  mvhf  32708  msubvrs  32710  iprodefisumlem  32875  filnetlem3  33631  knoppcnlem10  33744  knoppcnlem11  33745  icoreunrn  34528  icoreelrn  34530  ralssiun  34576  poimirlem3  34781  poimirlem16  34794  poimirlem17  34795  poimirlem19  34797  poimirlem30  34808  dvasin  34864  cover2  34876  upixp  34891  sdclem1  34905  fdc  34907  caushft  34923  ismtyres  34973  rrncmslem  34997  isfld2  35170  osumcllem10N  36987  pexmidlem7N  36998  dihglblem2N  38316  lcfrvalsnN  38563  lcfrlem5  38568  lcfrlem6  38569  lcfrlem27  38591  lcfrlem37  38601  prjspvs  39144  0prjspnrel  39153  monotuz  39422  expdiophlem1  39502  kelac2  39549  grurankcld  40453  dvgrat  40528  nzss  40533  uzmptshftfval  40562  binomcxplemnotnn0  40572  refsumcn  41171  rfcnpre2  41172  rfcnpre3  41174  rfcnpre4  41175  elabrexg  41187  disjf1o  41336  unirnmap  41355  unirnmapsn  41361  ssmapsn  41363  mptssid  41395  allbutfi  41549  eluzd  41566  uzidd2  41574  ressiocsup  41714  ressioosup  41715  ressiooinf  41717  fsumsermpt  41744  climexp  41770  climinf  41771  climsuse  41773  sumnnodd  41795  limsupresico  41865  limsupubuzlem  41877  limsupresxr  41931  liminfresxr  41932  liminfresico  41936  limsup10exlem  41937  cnrefiisplem  41994  cncfiooicclem1  42060  dvsinax  42081  itgsinexplem1  42123  fvvolioof  42159  fvvolicof  42161  stoweidlem14  42184  stoweidlem16  42186  stoweidlem31  42201  stoweidlem34  42204  stoweidlem36  42206  stoweidlem43  42213  stoweidlem46  42216  stoweidlem47  42217  stoweidlem52  42222  stoweidlem55  42225  stoweidlem57  42227  dirkercncf  42277  fourierdlem20  42297  fourierdlem42  42319  fourierdlem48  42324  fourierdlem49  42325  fourierdlem51  42327  fourierdlem54  42330  fourierdlem62  42338  fourierdlem71  42347  fourierdlem80  42356  fourierdlem114  42390  fouriersw  42401  ioorrnopnlem  42474  ioorrnopnxrlem  42476  salexct3  42510  salgencntex  42511  salgensscntex  42512  subsalsal  42527  sge0fodjrnlem  42583  sge0isum  42594  sge0seq  42613  sge0reuz  42614  sge0reuzb  42615  meadjiunlem  42632  meaiininclem  42653  carageniuncllem1  42688  caratheodorylem1  42693  hoiprodp1  42755  hoidmv1lelem1  42758  hoidmv1lelem2  42759  hoidmv1le  42761  hoidmvlelem1  42762  hoidmvlelem2  42763  hoidmvlelem3  42764  voncmpl  42788  hoiqssbl  42792  smflimlem2  42933  smfsuplem1  42970  smfsuplem3  42972  afvres  43256  afv2res  43323  iccpartigtl  43434  sprsymrelf  43508  prproropf1olem2  43517  ushrisomgr  43857  funcringcsetcALTV2lem3  44211  funcringcsetclem3ALTV  44234  lindslinindsimp2lem5  44419  rrxsphere  44637  line2  44641  onsetreclem3  44711  amgmwlem  44805
  Copyright terms: Public domain W3C validator