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

Theorem syl6eleqr 2503
Description: A membership and equality inference. (Contributed by NM, 24-Apr-2005.)
Hypotheses
Ref Expression
syl6eleqr.1  |-  ( ph  ->  A  e.  B )
syl6eleqr.2  |-  C  =  B
Assertion
Ref Expression
syl6eleqr  |-  ( ph  ->  A  e.  C )

Proof of Theorem syl6eleqr
StepHypRef Expression
1 syl6eleqr.1 . 2  |-  ( ph  ->  A  e.  B )
2 syl6eleqr.2 . . 3  |-  C  =  B
32eqcomi 2416 . 2  |-  B  =  C
41, 3syl6eleq 2502 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1721
This theorem is referenced by:  brelrng  5066  elabrex  5952  fliftel1  5999  ovidig  6158  unielxp  6352  riotacl2  6530  tfrlem11  6616  rdglim  6651  seqomlem4  6677  2oconcl  6714  ecopqsi  6928  erov  6968  eroprf  6969  sbthlem2  7185  dffi3  7402  ixpiunwdom  7523  cantnfcl  7586  r1lim  7662  rankwflemb  7683  pwwf  7697  unwf  7700  rankwflem  7705  uniwf  7709  rankpwi  7713  rankr1g  7722  r1pw  7735  r1rankid  7749  rankuni  7753  cardlim  7823  infxpenlem  7859  alephfp  7953  cfsmolem  8114  alephsing  8120  hsmexlem4  8273  numth3  8314  iunfo  8378  konigthlem  8407  iunctb  8413  canthwelem  8489  canthwe  8490  r1limwun  8575  inar1  8614  inatsk  8617  gruina  8657  grur1  8659  tskmval  8678  tskmcl  8680  pinq  8768  dmrecnq  8809  addclsr  8922  mulclsr  8923  axaddf  8984  axmulf  8985  peano2nn  9976  uztrn2  10467  peano2uzs  10495  uzsupss  10532  uzsup  11207  uzrdgfni  11261  uzrdgsuci  11263  seqf  11307  ser0  11338  bcm1k  11569  bcp1nk  11571  bcpasc  11575  fz1isolem  11673  rexuzre  12119  limsupgre  12238  climconst  12300  rlimclim1  12302  climrlim2  12304  clim2ser  12411  clim2ser2  12412  iserex  12413  isermulc2  12414  iserle  12416  isercolllem3  12423  isercoll2  12425  climsup  12426  iseraltlem2  12439  iseraltlem3  12440  isumclim3  12506  isumadd  12514  fsump1i  12516  iserabs  12557  cvgcmp  12558  cvgcmpub  12559  cvgcmpce  12560  abscvgcvg  12561  isumshft  12582  isumsplit  12583  isum1p  12584  isumrpcl  12586  isumsup2  12589  climcndslem1  12592  cvgrat  12623  ef0lem  12644  rpnnen2lem3  12779  fzo0dvdseq  12865  bitsinv1  12917  smupval  12963  smueqlem  12965  seq1st  13025  algr0  13026  prmind2  13053  crt  13130  eulerthlem2  13134  prmdiv  13137  pockthlem  13236  pockthg  13237  unbenlem  13239  prmunb  13245  strfv2d  13462  imasvscaval  13726  oppccatid  13908  epii  13932  fthepi  14088  yon12  14325  yon2  14326  yonedalem4c  14337  yonedalem22  14338  yonedalem3b  14339  yonedainv  14341  acsmapd  14567  cntrsubgnsg  15102  gexcl3  15184  efgi  15314  efgi2  15320  efgs1b  15331  efgredlemg  15337  efgredlemd  15339  frgpnabllem1  15447  cycsubgcyg  15473  gsumzaddlem  15489  dprd2da  15563  lsppratlem3  16184  lsppratlem4  16185  lbsextlem2  16194  lidl0  16253  lidl1  16254  mplsubrglem  16465  domnchr  16776  znf1o  16795  isclo  17114  indiscld  17118  restntr  17208  ordtbaslem  17214  ordtbas2  17217  lmconst  17287  lmss  17324  concompid  17455  2ndcomap  17482  xkouni  17592  txcls  17597  ptclsg  17608  uptx  17618  txindis  17627  tx1stc  17643  cnmpt1res  17669  tgqtop  17705  uffix  17914  cnpflf2  17993  ptcmplem2  18045  ptcmplem4  18047  tgpconcomp  18103  tsmsfbas  18118  fmucnd  18283  prdsxmetlem  18359  imasdsf1olem  18364  prdsbl  18482  blcvx  18790  xrsmopn  18804  xrge0tsms  18826  metdcn2  18831  cnmpt2pc  18914  icchmeo  18927  iccpnfhmeo  18931  cnheibor  18941  evth  18945  evth2  18946  lebnumlem2  18948  lebnumii  18952  reparphti  18983  cfilfcls  19188  minveclem2  19288  minveclem3  19291  minveclem4  19294  ovoliunlem1  19359  ovolicc1  19373  iundisj  19403  iunmbl  19408  volsup  19411  uniioombllem3  19438  vitalilem2  19462  vitalilem3  19463  mbfsup  19517  mbfinf  19518  mbflimsup  19519  itg2monolem1  19603  limcflflem  19728  limccnp  19739  limccnp2  19740  dvidlem  19763  dvn2bss  19777  cpnres  19784  dvcobr  19793  dvrec  19802  c1liplem1  19841  dvcnvrelem2  19863  dvfsumrlimf  19870  dvfsumlem1  19871  dvfsumlem2  19872  dvfsumlem3  19873  dvfsumlem4  19874  dvfsumrlim  19876  dvfsum2  19879  mpfconst  19920  mpfproj  19921  mpfind  19926  pf1const  19927  pf1id  19928  mpfpf1  19932  pf1mpf  19933  coeeulem  20104  coeid3  20120  plycn  20140  dvntaylp  20248  taylthlem1  20250  taylthlem2  20251  ulm2  20262  ulmshftlem  20266  ulmshft  20267  ulm0  20268  ulmcn  20276  ulmdvlem3  20279  ulmdv  20280  mtest  20281  mtestbdd  20282  dvradcnv  20298  psercn2  20300  psercn  20303  pserdv  20306  abelth  20318  efif1olem2  20406  efif1olem4  20408  efifo  20410  eff1olem  20411  logcn  20499  dvloglem  20500  advlogexp  20507  cxpcn3  20593  resqrcn  20594  sqrcn  20595  asinneg  20687  atanlogsub  20717  atanbnd  20727  ressatans  20735  leibpilem2  20742  xrlimcnp  20768  efrlim  20769  scvxcvx  20785  dvdsflip  20928  ppiub  20949  chtub  20957  logexprlim  20970  lgseisenlem1  21094  rplogsumlem1  21139  rplogsumlem2  21140  dchrisumlem2  21145  dchrisum0flb  21165  logdivbnd  21211  pntlem3  21264  nbgraf1olem3  21414  cusgrares  21442  eupap1  21659  isgrpo2  21746  minvecolem1  22337  minvecolem2  22338  minvecolem4  22343  htthlem  22381  5oalem2  23118  3oalem2  23126  iundisjf  23990  xppreima  24020  xppreima2  24021  xrge0tsmsd  24184  rhmopp  24218  tpr2rico  24271  xrmulc1cn  24277  xrge0mulc1cn  24288  logblt  24367  esumpfinvallem  24425  brfae  24560  sxbrsigalem3  24583  dya2icoseg2  24589  sibfof  24615  probfinmeasbOLD  24647  subfacp1lem5  24831  subfacp1lem6  24832  cvxpcon  24890  cvxscon  24891  cvmliftlem6  24938  cvmliftlem8  24940  cvmliftlem10  24942  cvmlift2lem6  24956  cvmlift2lem11  24961  cvmlift2lem12  24962  clim2prod  25177  clim2div  25178  prodf1  25180  ntrivcvgn0  25187  ntrivcvgtail  25189  fprodntriv  25229  fprodabs  25258  fprodefsum  25259  fprodeq0  25260  iprodclim3  25274  iprodmul  25277  iprodefisumlem  25278  nobndlem2  25569  nobndlem6  25573  nofulllem3  25580  locfincmp  26282  comppfsc  26285  filnetlem3  26307  cover2  26313  upixp  26329  sdclem1  26345  fdc  26347  caushft  26365  ismtyres  26415  rrncmslem  26439  isfld2  26513  monotuz  26902  expdiophlem1  26990  kelac2  27039  pmtrrn  27275  refsumcn  27576  rfcnpre2  27577  rfcnpre3  27579  rfcnpre4  27580  expcncf  27598  climexp  27606  climinf  27607  climsuse  27609  itgsinexplem1  27623  stoweidlem14  27638  stoweidlem16  27640  stoweidlem31  27655  stoweidlem34  27658  stoweidlem36  27660  stoweidlem43  27667  stoweidlem46  27670  stoweidlem47  27671  stoweidlem52  27676  stoweidlem55  27679  stoweidlem57  27681  afvres  27911  ubmelm1fzo  27995  swrdccatin12lem4  28033  bnj1379  28920  osumcllem10N  30459  pexmidlem7N  30470  dihglblem2N  31789  lcfrvalsnN  32036  lcfrlem5  32041  lcfrlem6  32042  lcfrlem27  32064  lcfrlem37  32074
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2405  df-clel 2408
  Copyright terms: Public domain W3C validator