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

Theorem syl6eleqr 2495
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 2408 . 2  |-  B  =  C
41, 3syl6eleq 2494 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  5058  elabrex  5944  fliftel1  5991  ovidig  6150  unielxp  6344  riotacl2  6522  tfrlem11  6608  rdglim  6643  seqomlem4  6669  2oconcl  6706  ecopqsi  6920  erov  6960  eroprf  6961  sbthlem2  7177  dffi3  7394  ixpiunwdom  7515  cantnfcl  7578  r1lim  7654  rankwflemb  7675  pwwf  7689  unwf  7692  rankwflem  7697  uniwf  7701  rankpwi  7705  rankr1g  7714  r1pw  7727  r1rankid  7741  rankuni  7745  cardlim  7815  infxpenlem  7851  alephfp  7945  cfsmolem  8106  alephsing  8112  hsmexlem4  8265  numth3  8306  iunfo  8370  konigthlem  8399  iunctb  8405  canthwelem  8481  canthwe  8482  r1limwun  8567  inar1  8606  inatsk  8609  gruina  8649  grur1  8651  tskmval  8670  tskmcl  8672  pinq  8760  dmrecnq  8801  addclsr  8914  mulclsr  8915  axaddf  8976  axmulf  8977  peano2nn  9968  uztrn2  10459  peano2uzs  10487  uzsupss  10524  uzsup  11199  uzrdgfni  11253  uzrdgsuci  11255  seqf  11299  ser0  11330  bcm1k  11561  bcp1nk  11563  bcpasc  11567  fz1isolem  11665  rexuzre  12111  limsupgre  12230  climconst  12292  rlimclim1  12294  climrlim2  12296  clim2ser  12403  clim2ser2  12404  iserex  12405  isermulc2  12406  iserle  12408  isercolllem3  12415  isercoll2  12417  climsup  12418  iseraltlem2  12431  iseraltlem3  12432  isumclim3  12498  isumadd  12506  fsump1i  12508  iserabs  12549  cvgcmp  12550  cvgcmpub  12551  cvgcmpce  12552  abscvgcvg  12553  isumshft  12574  isumsplit  12575  isum1p  12576  isumrpcl  12578  isumsup2  12581  climcndslem1  12584  cvgrat  12615  ef0lem  12636  rpnnen2lem3  12771  fzo0dvdseq  12857  bitsinv1  12909  smupval  12955  smueqlem  12957  seq1st  13017  algr0  13018  prmind2  13045  crt  13122  eulerthlem2  13126  prmdiv  13129  pockthlem  13228  pockthg  13229  unbenlem  13231  prmunb  13237  strfv2d  13454  imasvscaval  13718  oppccatid  13900  epii  13924  fthepi  14080  yon12  14317  yon2  14318  yonedalem4c  14329  yonedalem22  14330  yonedalem3b  14331  yonedainv  14333  acsmapd  14559  cntrsubgnsg  15094  gexcl3  15176  efgi  15306  efgi2  15312  efgs1b  15323  efgredlemg  15329  efgredlemd  15331  frgpnabllem1  15439  cycsubgcyg  15465  gsumzaddlem  15481  dprd2da  15555  lsppratlem3  16176  lsppratlem4  16177  lbsextlem2  16186  lidl0  16245  lidl1  16246  mplsubrglem  16457  domnchr  16768  znf1o  16787  isclo  17106  indiscld  17110  restntr  17200  ordtbaslem  17206  ordtbas2  17209  lmconst  17279  lmss  17316  concompid  17447  2ndcomap  17474  xkouni  17584  txcls  17589  ptclsg  17600  uptx  17610  txindis  17619  tx1stc  17635  cnmpt1res  17661  tgqtop  17697  uffix  17906  cnpflf2  17985  ptcmplem2  18037  ptcmplem4  18039  tgpconcomp  18095  tsmsfbas  18110  fmucnd  18275  prdsxmetlem  18351  imasdsf1olem  18356  prdsbl  18474  blcvx  18782  xrsmopn  18796  xrge0tsms  18818  metdcn2  18823  cnmpt2pc  18906  icchmeo  18919  iccpnfhmeo  18923  cnheibor  18933  evth  18937  evth2  18938  lebnumlem2  18940  lebnumii  18944  reparphti  18975  cfilfcls  19180  minveclem2  19280  minveclem3  19283  minveclem4  19286  ovoliunlem1  19351  ovolicc1  19365  iundisj  19395  iunmbl  19400  volsup  19403  uniioombllem3  19430  vitalilem2  19454  vitalilem3  19455  mbfsup  19509  mbfinf  19510  mbflimsup  19511  itg2monolem1  19595  limcflflem  19720  limccnp  19731  limccnp2  19732  dvidlem  19755  dvn2bss  19769  cpnres  19776  dvcobr  19785  dvrec  19794  c1liplem1  19833  dvcnvrelem2  19855  dvfsumrlimf  19862  dvfsumlem1  19863  dvfsumlem2  19864  dvfsumlem3  19865  dvfsumlem4  19866  dvfsumrlim  19868  dvfsum2  19871  mpfconst  19912  mpfproj  19913  mpfind  19918  pf1const  19919  pf1id  19920  mpfpf1  19924  pf1mpf  19925  coeeulem  20096  coeid3  20112  plycn  20132  dvntaylp  20240  taylthlem1  20242  taylthlem2  20243  ulm2  20254  ulmshftlem  20258  ulmshft  20259  ulm0  20260  ulmcn  20268  ulmdvlem3  20271  ulmdv  20272  mtest  20273  mtestbdd  20274  dvradcnv  20290  psercn2  20292  psercn  20295  pserdv  20298  abelth  20310  efif1olem2  20398  efif1olem4  20400  efifo  20402  eff1olem  20403  logcn  20491  dvloglem  20492  advlogexp  20499  cxpcn3  20585  resqrcn  20586  sqrcn  20587  asinneg  20679  atanlogsub  20709  atanbnd  20719  ressatans  20727  leibpilem2  20734  xrlimcnp  20760  efrlim  20761  scvxcvx  20777  dvdsflip  20920  ppiub  20941  chtub  20949  logexprlim  20962  lgseisenlem1  21086  rplogsumlem1  21131  rplogsumlem2  21132  dchrisumlem2  21137  dchrisum0flb  21157  logdivbnd  21203  pntlem3  21256  nbgraf1olem3  21406  cusgrares  21434  eupap1  21651  isgrpo2  21738  minvecolem1  22329  minvecolem2  22330  minvecolem4  22335  htthlem  22373  5oalem2  23110  3oalem2  23118  iundisjf  23982  xppreima  24012  xppreima2  24013  xrge0tsmsd  24176  rhmopp  24210  tpr2rico  24263  xrmulc1cn  24269  xrge0mulc1cn  24280  logblt  24359  esumpfinvallem  24417  brfae  24552  sxbrsigalem3  24575  dya2icoseg2  24581  sibfof  24607  probfinmeasbOLD  24639  subfacp1lem5  24823  subfacp1lem6  24824  cvxpcon  24882  cvxscon  24883  cvmliftlem6  24930  cvmliftlem8  24932  cvmliftlem10  24934  cvmlift2lem6  24948  cvmlift2lem11  24953  cvmlift2lem12  24954  clim2prod  25169  clim2div  25170  prodf1  25172  ntrivcvgn0  25179  ntrivcvgtail  25181  fprodntriv  25221  fprodabs  25250  fprodefsum  25251  fprodeq0  25252  iprodclim3  25266  iprodmul  25269  iprodefisumlem  25270  nobndlem2  25561  nobndlem6  25565  nofulllem3  25572  locfincmp  26274  comppfsc  26277  filnetlem3  26299  cover2  26305  upixp  26321  sdclem1  26337  fdc  26339  caushft  26357  ismtyres  26407  rrncmslem  26431  isfld2  26505  monotuz  26894  expdiophlem1  26982  kelac2  27031  pmtrrn  27267  refsumcn  27568  rfcnpre2  27569  rfcnpre3  27571  rfcnpre4  27572  expcncf  27590  climexp  27598  climinf  27599  climsuse  27601  itgsinexplem1  27615  stoweidlem14  27630  stoweidlem16  27632  stoweidlem31  27647  stoweidlem34  27650  stoweidlem36  27652  stoweidlem43  27659  stoweidlem46  27662  stoweidlem47  27663  stoweidlem52  27668  stoweidlem55  27671  stoweidlem57  27673  afvres  27903  ubmelm1fzo  27987  swrdccatin12lem4  28025  bnj1379  28908  osumcllem10N  30447  pexmidlem7N  30458  dihglblem2N  31777  lcfrvalsnN  32024  lcfrlem5  32029  lcfrlem6  32030  lcfrlem27  32052  lcfrlem37  32062
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 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2397  df-clel 2400
  Copyright terms: Public domain W3C validator