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

Theorem syl6eleqr 2449
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 2362 . 2  |-  B  =  C
41, 3syl6eleq 2448 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1642    e. wcel 1710
This theorem is referenced by:  brelrng  4990  elabrex  5851  fliftel1  5896  ovidig  6052  unielxp  6245  riotacl2  6405  tfrlem11  6491  rdglim  6526  seqomlem4  6552  2oconcl  6589  ecopqsi  6803  erov  6843  eroprf  6844  sbthlem2  7060  dffi3  7274  ixpiunwdom  7395  cantnfcl  7458  r1lim  7534  rankwflemb  7555  pwwf  7569  unwf  7572  rankwflem  7577  uniwf  7581  rankpwi  7585  rankr1g  7594  r1pw  7607  r1rankid  7621  rankuni  7625  cardlim  7695  infxpenlem  7731  alephfp  7825  cfsmolem  7986  alephsing  7992  hsmexlem4  8145  numth3  8187  iunfo  8251  konigthlem  8280  iunctb  8286  canthwelem  8362  canthwe  8363  r1limwun  8448  wunex3  8453  inar1  8487  inatsk  8490  gruina  8530  grur1  8532  tskmval  8551  tskmcl  8553  pinq  8641  dmrecnq  8682  addclsr  8795  mulclsr  8796  axaddf  8857  axmulf  8858  peano2nn  9848  uztrn2  10337  peano2uzs  10365  uzsupss  10402  uzsup  11059  uzrdgfni  11113  uzrdgsuci  11115  seqf  11159  ser0  11190  bcm1k  11420  bcp1nk  11422  bcpasc  11426  fz1isolem  11495  rexuzre  11932  limsupgre  12051  climconst  12113  rlimclim1  12115  climrlim2  12117  clim2ser  12224  clim2ser2  12225  iserex  12226  isermulc2  12227  iserle  12229  isercolllem3  12236  isercoll2  12238  climsup  12239  iseraltlem2  12252  iseraltlem3  12253  isumclim3  12319  isumadd  12327  fsump1i  12329  iserabs  12370  cvgcmp  12371  cvgcmpub  12372  cvgcmpce  12373  abscvgcvg  12374  isumshft  12395  isumsplit  12396  isum1p  12397  isumrpcl  12399  isumsup2  12402  climcndslem1  12405  cvgrat  12436  ef0lem  12457  rpnnen2lem3  12592  fzo0dvdseq  12678  bitsinv1  12730  smupval  12776  smueqlem  12778  seq1st  12838  algr0  12839  prmind2  12866  crt  12943  eulerthlem2  12947  prmdiv  12950  pockthlem  13049  pockthg  13050  unbenlem  13052  prmunb  13058  strfv2d  13275  imasvscaval  13539  oppccatid  13721  epii  13745  fthepi  13901  hofcl  14132  yon12  14138  yon2  14139  yonedalem4c  14150  yonedalem22  14151  yonedalem3b  14152  yonedainv  14154  acsmapd  14380  cntrsubgnsg  14915  gexcl3  14997  efgi  15127  efgi2  15133  efgs1b  15144  efgredlemg  15150  efgredlemd  15152  frgpnabllem1  15260  cycsubgcyg  15286  gsumzaddlem  15302  dprd2da  15376  lsppratlem3  16001  lsppratlem4  16002  lbsextlem2  16011  lidl0  16070  lidl1  16071  mplsubrglem  16282  domnchr  16592  znf1o  16611  isclo  16930  indiscld  16934  restntr  17018  ordtbaslem  17024  ordtbas2  17027  lmconst  17097  lmss  17132  concompid  17263  2ndcomap  17290  xkouni  17400  txcls  17405  ptclsg  17415  uptx  17425  txindis  17434  tx1stc  17450  cnmpt1res  17476  tgqtop  17509  uffix  17718  cnpflf2  17797  ptcmplem2  17849  ptcmplem4  17851  tgpconcomp  17897  tsmsfbas  17912  prdsxmetlem  18034  imasdsf1olem  18039  prdsbl  18139  blcvx  18406  xrsmopn  18420  xrge0tsms  18442  metdcn2  18447  cdivcncf  18524  cnmpt2pc  18530  icchmeo  18543  iccpnfhmeo  18547  cnheibor  18557  evth  18561  evth2  18562  lebnumlem2  18564  lebnumii  18568  reparphti  18599  cfilfcls  18804  minveclem2  18894  minveclem3  18897  minveclem4  18900  ovoliunlem1  18965  ovolicc1  18979  iundisj  19009  iunmbl  19014  volsup  19017  uniioombllem3  19044  vitalilem2  19068  vitalilem3  19069  mbfsup  19123  mbfinf  19124  mbflimsup  19125  itg1addlem4  19158  itg2monolem1  19209  limcflflem  19334  limccnp  19345  limccnp2  19346  dvidlem  19369  dvn2bss  19383  cpnres  19390  dvcobr  19399  dvrec  19408  c1liplem1  19447  dvcnvrelem2  19469  dvfsumrlimf  19476  dvfsumlem1  19477  dvfsumlem2  19478  dvfsumlem3  19479  dvfsumlem4  19480  dvfsumrlim  19482  dvfsum2  19485  mpfconst  19526  mpfproj  19527  mpfind  19532  pf1const  19533  pf1id  19534  mpfpf1  19538  pf1mpf  19539  coeeulem  19710  coeid3  19726  plycn  19746  dvntaylp  19854  taylthlem1  19856  taylthlem2  19857  ulm2  19868  ulmshftlem  19872  ulmshft  19873  ulm0  19874  ulmcn  19882  ulmdvlem3  19885  ulmdv  19886  mtest  19887  mtestbdd  19888  dvradcnv  19904  psercn2  19906  psercn  19909  pserdv  19912  abelth  19924  efif1olem2  20012  efif1olem4  20014  efifo  20016  eff1olem  20017  logcn  20105  dvloglem  20106  advlogexp  20113  cxpcn3  20199  resqrcn  20200  sqrcn  20201  asinneg  20293  atanlogsub  20323  atanbnd  20333  ressatans  20341  leibpilem2  20348  xrlimcnp  20374  efrlim  20375  scvxcvx  20391  dvdsflip  20534  ppiub  20555  chtub  20563  logexprlim  20576  lgseisenlem1  20700  rplogsumlem1  20745  rplogsumlem2  20746  dchrisumlem2  20751  dchrisum0flb  20771  logdivbnd  20817  pntlem3  20870  isgrpo2  20976  minvecolem1  21567  minvecolem2  21568  minvecolem4  21573  htthlem  21611  5oalem2  22348  3oalem2  22356  iundisjf  23227  xppreima  23262  xppreima2  23263  xrge0tsmsd  23415  rhmopp  23423  tpr2rico  23466  xrmulc1cn  23472  xrge0mulc1cn  23483  elrnust  23528  esumpfinvallem  23730  brfae  23863  sxbrsigalem3  23886  dya2icoseg2  23892  probfinmeasbOLD  23935  subfacp1lem5  24119  subfacp1lem6  24120  cvxpcon  24177  cvxscon  24178  cvmliftlem6  24225  cvmliftlem8  24227  cvmliftlem10  24229  cvmlift2lem6  24243  cvmlift2lem11  24248  cvmlift2lem12  24249  eupap1  24304  clim2prod  24517  clim2div  24518  prodf1  24520  ntrivcvgn0  24527  ntrivcvgtail  24529  fprodntriv  24569  fprodabs  24598  fprodefsum  24599  fprodeq0  24600  iprodclim3  24607  iprodmul  24610  nobndlem2  24905  nobndlem6  24909  nofulllem3  24916  locfincmp  25628  comppfsc  25631  filnetlem3  25653  cover2  25682  upixp  25727  sdclem1  25777  fdc  25779  caushft  25801  txopnOLD  25811  txcldOLD  25812  ismtyres  25855  rrncmslem  25879  isfld2  25953  monotuz  26349  expdiophlem1  26437  kelac2  26486  pmtrrn  26722  refsumcn  27024  rfcnpre2  27025  expcncf  27046  climexp  27054  climinf  27055  itgsinexplem1  27071  stoweidlem14  27086  stoweidlem31  27103  stoweidlem34  27106  stoweidlem36  27108  stoweidlem43  27115  stoweidlem46  27118  stoweidlem47  27119  stoweidlem51  27123  stoweidlem52  27124  stoweidlem55  27127  stoweidlem57  27129  afvres  27360  nbgraf1olem3  27607  cusgrares  27635  bnj1379  28625  osumcllem10N  30223  pexmidlem7N  30234  dihglblem2N  31553  lcfrvalsnN  31800  lcfrlem5  31805  lcfrlem6  31806  lcfrlem27  31828  lcfrlem37  31838
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-cleq 2351  df-clel 2354
  Copyright terms: Public domain W3C validator