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

Theorem syl6eleqr 2374
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 2287 . 2  |-  B  =  C
41, 3syl6eleq 2373 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684
This theorem is referenced by:  brelrng  4908  elabrex  5765  fliftel1  5809  ovidig  5965  unielxp  6158  riotacl2  6318  tfrlem11  6404  rdglim  6439  seqomlem4  6465  2oconcl  6502  ecopqsi  6716  erov  6755  eroprf  6756  sbthlem2  6972  dffi3  7184  ixpiunwdom  7305  cantnfcl  7368  r1lim  7444  rankwflemb  7465  pwwf  7479  unwf  7482  rankwflem  7487  uniwf  7491  rankpwi  7495  rankr1g  7504  r1pw  7517  r1rankid  7531  rankuni  7535  cardlim  7605  infxpenlem  7641  alephfp  7735  cfsmolem  7896  alephsing  7902  hsmexlem4  8055  numth3  8097  iunfo  8161  konigthlem  8190  iunctb  8196  canthwelem  8272  canthwe  8273  r1limwun  8358  wunex3  8363  inar1  8397  inatsk  8400  gruina  8440  grur1  8442  tskmval  8461  tskmcl  8463  pinq  8551  dmrecnq  8592  addclsr  8705  mulclsr  8706  axaddf  8767  axmulf  8768  peano2nn  9758  uztrn2  10245  peano2uzs  10273  uzsupss  10310  uzsup  10967  uzrdgfni  11021  uzrdgsuci  11023  seqf  11067  ser0  11098  bcm1k  11327  bcp1nk  11329  bcpasc  11333  fz1isolem  11399  rexuzre  11836  limsupgre  11955  climconst  12017  rlimclim1  12019  climrlim2  12021  clim2ser  12128  clim2ser2  12129  iserex  12130  isermulc2  12131  iserle  12133  isercolllem3  12140  isercoll2  12142  climsup  12143  iseraltlem2  12155  iseraltlem3  12156  isumclim3  12222  isumadd  12230  fsump1i  12232  iserabs  12273  cvgcmp  12274  cvgcmpub  12275  cvgcmpce  12276  abscvgcvg  12277  isumshft  12298  isumsplit  12299  isum1p  12300  isumrpcl  12302  isumsup2  12305  climcndslem1  12308  cvgrat  12339  ef0lem  12360  rpnnen2lem3  12495  fzo0dvdseq  12581  bitsinv1  12633  smupval  12679  smueqlem  12681  seq1st  12741  algr0  12742  prmind2  12769  crt  12846  eulerthlem2  12850  prmdiv  12853  pockthlem  12952  pockthg  12953  unbenlem  12955  prmunb  12961  strfv2d  13178  imasvscaval  13440  oppccatid  13622  epii  13646  fthepi  13802  hofcl  14033  yon12  14039  yon2  14040  yonedalem4c  14051  yonedalem22  14052  yonedalem3b  14053  yonedainv  14055  acsmapd  14281  cntrsubgnsg  14816  gexcl3  14898  efgi  15028  efgi2  15034  efgs1b  15045  efgredlemg  15051  efgredlemd  15053  frgpnabllem1  15161  cycsubgcyg  15187  gsumzaddlem  15203  dprd2da  15277  lsppratlem3  15902  lsppratlem4  15903  lbsextlem2  15912  lidl0  15971  lidl1  15972  mplsubrglem  16183  domnchr  16486  znf1o  16505  isclo  16824  indiscld  16828  restntr  16912  ordtbaslem  16918  ordtbas2  16921  lmconst  16991  lmss  17026  concompid  17157  2ndcomap  17184  xkouni  17294  txcls  17299  ptclsg  17309  uptx  17319  txindis  17328  tx1stc  17344  cnmpt1res  17370  tgqtop  17403  uffix  17616  cnpflf2  17695  ptcmplem2  17747  ptcmplem4  17749  tgpconcomp  17795  tsmsfbas  17810  prdsxmetlem  17932  imasdsf1olem  17937  prdsbl  18037  blcvx  18304  xrsmopn  18318  xrge0tsms  18339  metdcn2  18344  cdivcncf  18420  cnmpt2pc  18426  icchmeo  18439  iccpnfhmeo  18443  cnheibor  18453  evth  18457  evth2  18458  lebnumlem2  18460  lebnumii  18464  reparphti  18495  cfilfcls  18700  minveclem2  18790  minveclem3  18793  minveclem4  18796  ovoliunlem1  18861  ovolicc1  18875  iundisj  18905  iunmbl  18910  volsup  18913  uniioombllem3  18940  vitalilem2  18964  vitalilem3  18965  mbfsup  19019  mbfinf  19020  mbflimsup  19021  itg1addlem4  19054  itg2monolem1  19105  limcflflem  19230  limccnp  19241  limccnp2  19242  dvidlem  19265  dvn2bss  19279  cpnres  19286  dvcobr  19295  dvrec  19304  c1liplem1  19343  dvcnvrelem2  19365  dvfsumrlimf  19372  dvfsumlem1  19373  dvfsumlem2  19374  dvfsumlem3  19375  dvfsumlem4  19376  dvfsumrlim  19378  dvfsum2  19381  mpfconst  19422  mpfproj  19423  mpfind  19428  pf1const  19429  pf1id  19430  mpfpf1  19434  pf1mpf  19435  coeeulem  19606  coeid3  19622  plycn  19642  dvntaylp  19750  taylthlem1  19752  taylthlem2  19753  ulm2  19764  ulmshftlem  19768  ulmshft  19769  ulm0  19770  ulmcn  19776  ulmdvlem3  19779  ulmdv  19780  mtest  19781  dvradcnv  19797  psercn2  19799  psercn  19802  pserdv  19805  abelth  19817  efif1olem2  19905  efif1olem4  19907  efifo  19909  eff1olem  19910  logcn  19994  dvloglem  19995  advlogexp  20002  cxpcn3  20088  resqrcn  20089  sqrcn  20090  asinneg  20182  atanlogsub  20212  atanbnd  20222  ressatans  20230  leibpilem2  20237  xrlimcnp  20263  efrlim  20264  scvxcvx  20280  dvdsflip  20422  ppiub  20443  chtub  20451  logexprlim  20464  lgseisenlem1  20588  rplogsumlem1  20633  rplogsumlem2  20634  dchrisumlem2  20639  dchrisum0flb  20659  logdivbnd  20705  pntlem3  20758  isgrpo2  20864  minvecolem1  21453  minvecolem2  21454  minvecolem4  21459  htthlem  21497  5oalem2  22234  3oalem2  22242  xppreima  23211  xppreima2  23212  tpr2rico  23296  xrmulc1cn  23303  xrge0mulc1cn  23323  iundisjf  23365  xrge0tsmsd  23382  esumpfinvallem  23442  probfinmeasbOLD  23631  subfacp1lem5  23715  subfacp1lem6  23716  cvxpcon  23773  cvxscon  23774  cvmliftlem6  23821  cvmliftlem8  23823  cvmliftlem10  23825  cvmlift2lem6  23839  cvmlift2lem11  23844  cvmlift2lem12  23845  eupap1  23900  nobndlem2  24347  nobndlem6  24351  nofulllem3  24358  dstr  25171  pre1befi2  25231  seqzp2  25355  intopcoaconc  25541  limfilnei  25561  prdnei  25573  cntrset  25602  idcatval2  25944  1iskle  25989  cndpv  26049  pgapspf  26052  pgapspf2  26053  locfincmp  26304  comppfsc  26307  filnetlem3  26329  cover2  26358  upixp  26403  sdclem1  26453  fdc  26455  caushft  26477  txopnOLD  26488  txcldOLD  26489  ismtyres  26532  rrncmslem  26556  isfld2  26630  monotuz  27026  expdiophlem1  27114  kelac2  27163  pmtrrn  27399  refsumcn  27701  rfcnpre2  27702  expcncf  27723  climexp  27731  climinf  27732  itgsinexplem1  27748  stoweidlem14  27763  stoweidlem31  27780  stoweidlem34  27783  stoweidlem36  27785  stoweidlem43  27792  stoweidlem46  27795  stoweidlem47  27796  stoweidlem51  27800  stoweidlem52  27801  stoweidlem55  27804  stoweidlem57  27806  afvres  28034  bnj1379  28863  osumcllem10N  30154  pexmidlem7N  30165  dihglblem2N  31484  lcfrvalsnN  31731  lcfrlem5  31736  lcfrlem6  31737  lcfrlem27  31759  lcfrlem37  31769
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-cleq 2276  df-clel 2279
  Copyright terms: Public domain W3C validator