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

Theorem syl6eleqr 2529
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 2442 . 2  |-  B  =  C
41, 3syl6eleq 2528 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    e. wcel 1726
This theorem is referenced by:  brelrng  5101  elabrex  5987  fliftel1  6034  ovidig  6193  unielxp  6387  riotacl2  6565  tfrlem11  6651  rdglim  6686  seqomlem4  6712  2oconcl  6749  ecopqsi  6963  erov  7003  eroprf  7004  sbthlem2  7220  dffi3  7438  ixpiunwdom  7561  cantnfcl  7624  r1lim  7700  rankwflemb  7721  pwwf  7735  unwf  7738  rankwflem  7743  uniwf  7747  rankpwi  7751  rankr1g  7760  r1pw  7773  r1rankid  7787  rankuni  7791  cardlim  7861  infxpenlem  7897  alephfp  7991  cfsmolem  8152  alephsing  8158  hsmexlem4  8311  numth3  8352  iunfo  8416  konigthlem  8445  iunctb  8451  canthwelem  8527  canthwe  8528  r1limwun  8613  inar1  8652  inatsk  8655  gruina  8695  grur1  8697  tskmval  8716  tskmcl  8718  pinq  8806  dmrecnq  8847  addclsr  8960  mulclsr  8961  axaddf  9022  axmulf  9023  peano2nn  10014  uztrn2  10505  peano2uzs  10533  uzsupss  10570  uzsup  11246  uzrdgfni  11300  uzrdgsuci  11302  seqf  11346  ser0  11377  bcm1k  11608  bcp1nk  11610  bcpasc  11614  fz1isolem  11712  rexuzre  12158  limsupgre  12277  climconst  12339  rlimclim1  12341  climrlim2  12343  clim2ser  12450  clim2ser2  12451  iserex  12452  isermulc2  12453  iserle  12455  isercolllem3  12462  isercoll2  12464  climsup  12465  iseraltlem2  12478  iseraltlem3  12479  isumclim3  12545  isumadd  12553  fsump1i  12555  iserabs  12596  cvgcmp  12597  cvgcmpub  12598  cvgcmpce  12599  abscvgcvg  12600  isumshft  12621  isumsplit  12622  isum1p  12623  isumrpcl  12625  isumsup2  12628  climcndslem1  12631  cvgrat  12662  ef0lem  12683  rpnnen2lem3  12818  fzo0dvdseq  12904  bitsinv1  12956  smupval  13002  smueqlem  13004  seq1st  13064  algr0  13065  prmind2  13092  crt  13169  eulerthlem2  13173  prmdiv  13176  pockthlem  13275  pockthg  13276  unbenlem  13278  prmunb  13284  strfv2d  13501  imasvscaval  13765  oppccatid  13947  epii  13971  fthepi  14127  yon12  14364  yon2  14365  yonedalem4c  14376  yonedalem22  14377  yonedalem3b  14378  yonedainv  14380  acsmapd  14606  cntrsubgnsg  15141  gexcl3  15223  efgi  15353  efgi2  15359  efgs1b  15370  efgredlemg  15376  efgredlemd  15378  frgpnabllem1  15486  cycsubgcyg  15512  gsumzaddlem  15528  dprd2da  15602  lsppratlem3  16223  lsppratlem4  16224  lbsextlem2  16233  lidl0  16292  lidl1  16293  mplsubrglem  16504  domnchr  16815  znf1o  16834  isclo  17153  indiscld  17157  restntr  17248  ordtbaslem  17254  ordtbas2  17257  lmconst  17327  lmss  17364  concompid  17496  2ndcomap  17523  xkouni  17633  txcls  17638  ptclsg  17649  uptx  17659  txindis  17668  tx1stc  17684  cnmpt1res  17710  tgqtop  17746  uffix  17955  cnpflf2  18034  ptcmplem2  18086  ptcmplem4  18088  tgpconcomp  18144  tsmsfbas  18159  fmucnd  18324  prdsxmetlem  18400  imasdsf1olem  18405  prdsbl  18523  blcvx  18831  xrsmopn  18845  xrge0tsms  18867  metdcn2  18872  cnmpt2pc  18955  icchmeo  18968  iccpnfhmeo  18972  cnheibor  18982  evth  18986  evth2  18987  lebnumlem2  18989  lebnumii  18993  reparphti  19024  cfilfcls  19229  minveclem2  19329  minveclem3  19332  minveclem4  19335  ovoliunlem1  19400  ovolicc1  19414  iundisj  19444  iunmbl  19449  volsup  19452  uniioombllem3  19479  vitalilem2  19503  vitalilem3  19504  mbfsup  19558  mbfinf  19559  mbflimsup  19560  itg2monolem1  19644  limcflflem  19769  limccnp  19780  limccnp2  19781  dvidlem  19804  dvn2bss  19818  cpnres  19825  dvcobr  19834  dvrec  19843  c1liplem1  19882  dvcnvrelem2  19904  dvfsumrlimf  19911  dvfsumlem1  19912  dvfsumlem2  19913  dvfsumlem3  19914  dvfsumlem4  19915  dvfsumrlim  19917  dvfsum2  19920  mpfconst  19961  mpfproj  19962  mpfind  19967  pf1const  19968  pf1id  19969  mpfpf1  19973  pf1mpf  19974  coeeulem  20145  coeid3  20161  plycn  20181  dvntaylp  20289  taylthlem1  20291  taylthlem2  20292  ulm2  20303  ulmshftlem  20307  ulmshft  20308  ulm0  20309  ulmcn  20317  ulmdvlem3  20320  ulmdv  20321  mtest  20322  mtestbdd  20323  dvradcnv  20339  psercn2  20341  psercn  20344  pserdv  20347  abelth  20359  efif1olem2  20447  efif1olem4  20449  efifo  20451  eff1olem  20452  logcn  20540  dvloglem  20541  advlogexp  20548  cxpcn3  20634  resqrcn  20635  sqrcn  20636  asinneg  20728  atanlogsub  20758  atanbnd  20768  ressatans  20776  leibpilem2  20783  xrlimcnp  20809  efrlim  20810  scvxcvx  20826  dvdsflip  20969  ppiub  20990  chtub  20998  logexprlim  21011  lgseisenlem1  21135  rplogsumlem1  21180  rplogsumlem2  21181  dchrisumlem2  21186  dchrisum0flb  21206  logdivbnd  21252  pntlem3  21305  nbgraf1olem3  21455  cusgrares  21483  eupap1  21700  isgrpo2  21787  minvecolem1  22378  minvecolem2  22379  minvecolem4  22384  htthlem  22422  5oalem2  23159  3oalem2  23167  iundisjf  24031  xppreima  24061  xppreima2  24062  xrge0tsmsd  24225  rhmopp  24259  tpr2rico  24312  xrmulc1cn  24318  xrge0mulc1cn  24329  logblt  24408  esumpfinvallem  24466  brfae  24601  sxbrsigalem3  24624  dya2icoseg2  24630  sibfof  24656  probfinmeasbOLD  24688  subfacp1lem5  24872  subfacp1lem6  24873  cvxpcon  24931  cvxscon  24932  cvmliftlem6  24979  cvmliftlem8  24981  cvmliftlem10  24983  cvmlift2lem6  24997  cvmlift2lem11  25002  cvmlift2lem12  25003  clim2prod  25218  clim2div  25219  prodf1  25221  ntrivcvgn0  25228  ntrivcvgtail  25230  fprodntriv  25270  fprodabs  25299  fprodefsum  25300  fprodeq0  25301  iprodclim3  25315  iprodmul  25318  iprodefisumlem  25319  nobndlem2  25650  nobndlem6  25654  nofulllem3  25661  locfincmp  26386  comppfsc  26389  filnetlem3  26411  cover2  26417  upixp  26433  sdclem1  26449  fdc  26451  caushft  26469  ismtyres  26519  rrncmslem  26543  isfld2  26617  monotuz  27006  expdiophlem1  27094  kelac2  27142  pmtrrn  27378  refsumcn  27679  rfcnpre2  27680  rfcnpre3  27682  rfcnpre4  27683  expcncf  27701  climexp  27709  climinf  27710  climsuse  27712  itgsinexplem1  27726  stoweidlem14  27741  stoweidlem16  27743  stoweidlem31  27758  stoweidlem34  27761  stoweidlem36  27763  stoweidlem43  27770  stoweidlem46  27773  stoweidlem47  27774  stoweidlem52  27779  stoweidlem55  27782  stoweidlem57  27784  afvres  28014  ubmelm1fzo  28138  swrdccatin12lem4  28235  bnj1379  29264  osumcllem10N  30824  pexmidlem7N  30835  dihglblem2N  32154  lcfrvalsnN  32401  lcfrlem5  32406  lcfrlem6  32407  lcfrlem27  32429  lcfrlem37  32439
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-cleq 2431  df-clel 2434
  Copyright terms: Public domain W3C validator