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

Theorem syl5eqel 2517
Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
Hypotheses
Ref Expression
syl5eqel.1  |-  A  =  B
syl5eqel.2  |-  ( ph  ->  B  e.  C )
Assertion
Ref Expression
syl5eqel  |-  ( ph  ->  A  e.  C )

Proof of Theorem syl5eqel
StepHypRef Expression
1 syl5eqel.1 . . 3  |-  A  =  B
21a1i 11 . 2  |-  ( ph  ->  A  =  B )
3 syl5eqel.2 . 2  |-  ( ph  ->  B  e.  C )
42, 3eqeltrd 2507 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362    e. wcel 1755
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-cleq 2426  df-clel 2429
This theorem is referenced by:  syl5eqelr  2518  csbexg  4412  csbexgOLD  4414  rabexd  4432  snex  4521  dmresexg  5121  riotaprop  6064  fovrn  6222  fnovrn  6227  ovima0  6231  f1oabexg  6525  cofunexg  6530  cofunex2g  6531  abrexex2g  6543  xpexgALT  6559  opiota  6622  fnwelem  6676  mptsuppdifd  6700  tfrlem12  6834  rdgseg  6864  oelim2  7022  oeeulem  7028  ecexg  7093  qsexg  7146  pmex  7207  resixpfo  7289  elixpsn  7290  unxpdomlem3  7507  rabfi  7525  fnfi  7577  rnfi  7584  iunfi  7587  unifi  7588  pwfilem  7593  fsuppun  7627  fsuppcolem  7638  mapfienlem2  7643  supexd  7691  cantnfp1lem1  7874  oemapvali  7880  mapfienOLD  7915  wemapwe  7916  wemapweOLD  7917  cnfcomlem  7920  cnfcom  7921  cnfcom2lem  7922  cnfcom2  7923  cnfcom3lem  7924  cnfcom3  7925  cnfcomlemOLD  7928  cnfcomOLD  7929  cnfcom2lemOLD  7930  cnfcom2OLD  7931  cnfcom3lemOLD  7932  cnfcom3OLD  7933  prwf  8006  scott0  8081  htalem  8091  infxpenlem  8168  dfac8b  8189  cfss  8422  cofsmo  8426  coftr  8430  fin1a2lem10  8566  hsmexlem4  8586  hsmex2  8590  fpwwe  8801  canthwelem  8805  pwfseqlem1  8813  wuntp  8866  wunsn  8871  wunsuc  8872  wunr1om  8874  wunot  8878  r1limwun  8891  tsk1  8919  tsk2  8920  tskr1om  8922  gruuni  8955  grusn  8959  gruina  8973  wuncn  9325  negcl  9598  peano5nni  10313  peano5uzi  10718  quoremz  11678  quoremnn0  11679  quoremnn0ALT  11680  intfrac2  11681  intfracq  11682  seqf1olem1  11829  seqf1olem2  11830  serle  11845  discr1  11984  swrdccatin2  12362  swrdccatin12lem2  12364  swrdccatin12  12366  swrdccat3  12367  swrdccat3a  12369  cats1cld  12466  sqrlem4  12719  sqreulem  12831  reccn2  13058  fsump1i  13220  fsumabs  13247  o1fsum  13259  supcvg  13301  mertenslem1  13327  mertenslem2  13328  rpnnen2  13491  ruclem12  13506  bitsfzolem  13613  bezoutlem2  13706  algrf  13731  algcvg  13734  algcvga  13737  algfx  13738  eucalgcvga  13744  eucalg  13745  prmdiv  13843  pythagtriplem11  13875  pythagtriplem13  13877  pcprecl  13889  infpnlem1  13954  infpnlem2  13955  4sqlem5  13986  mul4sqlem  13997  4sqlem13  14001  4sqlem14  14002  4sqlem17  14005  4sqlem18  14006  vdwlem5  14029  wunndx  14173  wunress  14220  restid  14355  mreexdomd  14570  acsfn0  14581  acsfn1  14582  acsfn2  14584  funcf2  14761  funcpropd  14793  fthepi  14821  ressffth  14831  elhomai2  14885  catcxpccl  15000  diag1cl  15035  yonedalem1  15065  prdsinvlem  15643  subggrp  15664  nsgacs  15697  ghmima  15747  gimco  15776  gicref  15779  cntrnsg  15839  oppgmnd  15849  cayley  15899  symgfixfolem1  15924  pmtrdifellem1  15962  psgndmsubg  15988  efgredlemf  16218  efgredlemd  16221  efgredlemc  16222  cycsubgcyg  16357  gsumzaddlem  16388  gsumzaddlemOLD  16390  gsum2dlem1  16435  gsum2dlem2  16436  gsum2dOLD  16438  dprdfid  16481  dprdfidOLD  16488  dprd2dlem1  16514  dprd2da  16515  ablfacrplem  16540  ablfacrp  16541  ablfacrp2  16542  ablfac1lem  16543  pgpfac1lem1  16549  pgpfac1lem2  16550  pgpfac1lem3a  16551  pgpfac1lem3  16552  pgpfac1lem4  16553  pgpfac1lem5  16554  pgpfaclem1  16556  ablfaclem3  16562  opprrng  16657  subrgrng  16792  lmhmkerlss  17054  rlmlmod  17208  lidl0cl  17216  lidlacl  17217  lidlnegcl  17218  lidlmcl  17221  lidlacs  17225  fidomndrnglem  17300  gsumbagdiag  17380  psrass1lem  17381  psrlidm  17408  psrridm  17410  mplsubrglem  17451  mplsubrglemOLD  17452  vr1cl2  17548  vr1cl  17570  subrgvr1cl  17614  zringlpirlem2  17746  zringlpirlem3  17747  zlpirlem2  17751  zlpirlem3  17752  cygznlem1  17841  cygznlem2a  17842  cygznlem3  17844  isphld  17925  lindsmm  18099  1marepvmarrepid  18228  1marepvsma1  18236  mdetleib2  18241  smadiadetlem3  18316  cramerimplem1  18331  cramerimplem2  18332  cramerimplem3  18333  cramerimp  18334  topopn  18361  rintopn  18364  fctop  18450  topcld  18481  intcld  18486  uncld  18487  unicld  18492  mretopd  18538  neiptoptop  18577  tgrest  18605  restin  18612  neitr  18626  restcls  18627  restntr  18628  restlp  18629  restperf  18630  perfopn  18631  ordtbaslem  18634  ordtuni  18636  ordtbas2  18637  ordtbas  18638  ordttopon  18639  ordtopn1  18640  ordtopn2  18641  ordtrest2lem  18649  ordtrest2  18650  cnco  18712  cnrest  18731  cnprest2  18736  lmss  18744  cncmp  18837  imacmp  18842  fiuncmp  18849  bwthOLD  18856  concompcon  18878  cldllycmp  18941  hausmapdom  18946  kgentopon  18953  1stckgen  18969  ptbasin  18992  ptbasfi  18996  pttopon  19011  xkotopon  19015  txbasval  19021  ptpjcn  19026  ptcldmpt  19029  dfac14lem  19032  txcn  19041  ptcn  19042  ptrescn  19054  txkgen  19067  cnmpt12f  19081  xkofvcn  19099  qtopval2  19111  elqtop  19112  qtoptop2  19114  hmeoco  19187  idhmeo  19188  ordthmeolem  19216  ptunhmeo  19223  xkohmeo  19230  qtopf1  19231  cfinfil  19308  ufprim  19324  ufildr  19346  fin1aufil  19347  fmfg  19364  elfm3  19365  fbflim  19391  flimclslem  19399  flffbas  19410  cnpflf2  19415  flfcnp2  19422  fclsbas  19436  alexsublem  19458  ptcmplem3  19468  ptcmpg  19471  cnextcn  19481  tgpsubcn  19503  tmdgsum  19508  symgtgp  19514  tmdlactcn  19515  submtmd  19517  clssubg  19521  divstgplem  19533  prdstmdd  19536  tsmsfbas  19540  eltsms  19545  tsmssubm  19558  dvrcn  19600  utop2nei  19667  utop3cls  19668  utopreg  19669  blres  19848  prdsbl  19908  metrest  19941  metustexhalfOLD  19980  metustexhalf  19981  subgngp  20063  nlmvscnlem2  20108  nlmvscnlem1  20109  nrginvrcnlem  20113  qtopbaslem  20179  tgqioo  20219  icccmplem2  20242  icccmp  20244  reconnlem2  20246  xrge0tsms  20253  nmcn  20263  metnrmlem2  20278  divcn  20286  fsumcn  20288  fsum2cn  20289  cncfmet  20326  addccncf  20334  cnmpt2pc  20342  icchmeo  20355  cnrehmeo  20367  cnheiborlem  20368  bndth  20372  lebnumlem2  20376  htpycom  20390  htpyid  20391  htpyco1  20392  htpycc  20394  reparphti  20411  pcohtpylem  20433  pcoptcl  20435  pcoass  20438  pcorevcl  20439  pcorevlem  20440  ipcnlem2  20598  ipcnlem1  20599  cmsss  20703  minveclem4c  20754  minveclem3b  20757  minveclem4a  20759  minveclem4  20761  minveclem6  20763  pjthlem1  20766  ivthlem2  20778  ivthlem3  20779  ovolicc2lem4  20845  finiunmbl  20867  voliunlem1  20873  ioombl1lem1  20881  ioombl1lem3  20883  ioombl1lem4  20884  ovolioo  20891  opnmblALT  20925  mbfimaicc  20953  mbfid  20956  mbfeqalem  20962  mbfres  20964  cncombf  20978  mbfi1flim  21043  itg2monolem2  21071  itg2monolem3  21072  itg2mono  21073  itg2cnlem1  21081  itgcl  21103  iblss  21124  itgeqa  21133  itgss3  21134  itgless  21136  iblconst  21137  ibladdlem  21139  itgaddlem1  21142  iblabslem  21147  iblabsr  21149  iblmulc2  21150  itggt0  21161  itgcn  21162  limcvallem  21188  limcflflem  21197  limcres  21203  cnplimc  21204  limccnp  21208  limccnp2  21209  dvreslem  21226  dvres2lem  21227  dvcnp  21235  dvnff  21239  dvmptres2  21278  dvmptres  21279  dvmptntr  21287  dvmptfsum  21289  dvcnvlem  21290  dvcnv  21291  dvferm1lem  21298  dvferm2lem  21300  dvlipcn  21308  dvlip2  21309  c1liplem1  21310  lhop1lem  21327  dvcnvrelem2  21332  dvcvx  21334  dvfsumge  21336  dvfsumlem3  21342  ftc1lem3  21352  ftc1lem4  21353  evl1rhm  21380  mdegleb  21420  ply1remlem  21519  ply0  21561  plyid  21562  plyeq0lem  21563  dgrub  21587  dgrub2  21588  dgrlb  21589  coeidlem  21590  coeaddlem  21601  coemullem  21602  coemulhi  21606  dgreq0  21617  dgrlt  21618  dgradd2  21620  dgrmul  21622  dgrcolem2  21626  dgrco  21627  plycj  21629  coecj  21630  plydivlem2  21645  plydivlem4  21647  plyremlem  21655  plyrem  21656  quotcan  21660  vieta1lem1  21661  elqaalem2  21671  elqaalem3  21672  radcnvcl  21767  psercnlem1  21775  pserdvlem2  21778  pilem2  21802  pilem3  21803  logfac  21934  logcnlem2  21973  logcnlem3  21974  logcnlem4  21975  dvlog  21981  cxpcn  22068  cxpcn3lem  22070  ang180lem1  22090  ang180lem2  22091  ang180lem3  22092  pythag  22098  heron  22118  quart1lem  22135  xrlimcnp  22247  efrlim  22248  ftalem1  22295  ftalem2  22296  ftalem4  22298  ftalem5  22299  basellem1  22303  basellem2  22304  basellem3  22305  basellem4  22306  basellem5  22307  basellem8  22310  dchr1cl  22475  dchrinvcl  22477  dchrptlem1  22488  dchrptlem2  22489  bposlem3  22510  bposlem5  22512  bposlem6  22513  lgsqrlem2  22566  lgsqrlem3  22567  lgsqrlem4  22568  lgseisenlem1  22573  lgseisenlem2  22574  lgseisenlem3  22575  lgseisenlem4  22576  lgsquadlem1  22578  lgsquadlem2  22579  lgsquadlem3  22580  2sqlem8  22596  chebbnd1lem1  22603  chebbnd1lem2  22604  chebbnd1lem3  22605  mulog2sumlem2  22669  selberglem2  22680  chpdifbndlem1  22687  chpdifbndlem2  22688  pntrmax  22698  pntpbnd1a  22719  pntpbnd1  22720  pntpbnd2  22721  pntibndlem1  22723  pntibndlem2  22725  pntibndlem3  22726  pntlemd  22728  pntlemc  22729  pntlema  22730  pntlemg  22732  pntlemr  22736  pntlemj  22737  ostth2lem2  22768  ostth2lem3  22769  ostth2lem4  22770  ostth2  22771  ostth3  22772  tgelrnln  22907  eleesub  22980  axsegconlem2  22987  axsegconlem8  22993  axlowdimlem7  23017  axlowdimlem17  23027  usgrares1  23146  usgrafilem2  23148  cusgraexilem1  23197  cusgrares  23203  cusgrasizeinds  23207  cusgrafilem3  23212  wlks  23248  trls  23258  grpoinvfval  23534  grpodivfval  23552  gxfval  23567  ghgrp  23678  isvc  23782  isnv  23813  imsmet  23905  smcnlem  23915  minvecolem2  24099  minvecolem3  24100  minvecolem4c  24103  minvecolem4  24104  minvecolem5  24105  minvecolem6  24106  hhssabloi  24486  pjhthlem1  24617  pjoc1i  24657  cnlnadjlem3  25296  cnlnadjlem5  25298  mdsymlem1  25630  mdsymlem3  25632  abrexexd  25714  elovimad  25780  gsumle  26098  gsummpt2co  26101  ordtconlem1  26208  xrge0pluscn  26224  prsiga  26428  inelsiga  26432  mbfmcst  26528  mbfmco  26533  mbfmcnt  26537  dya2icoseg  26546  sibf0  26568  sibff  26570  sibfinima  26573  sibfof  26574  sitgclg  26576  eulerpartlemt  26602  sseqval  26619  0rrv  26682  rrvsum  26685  signsplypnf  26799  signsply0  26800  signsvtn0  26819  signstfveq0a  26825  signstfveq0  26826  signsvtp  26832  signsvtn  26833  signsvfpn  26834  signsvfnn  26835  erdsze2lem1  26939  erdsze2lem2  26940  txsconlem  26977  cvxpcon  26979  cvxscon  26980  cvmsiota  27014  cvmliftiota  27038  cvmlift2lem10  27049  ghomgrp  27156  wsucex  27610  wsuccl  27611  nobndlem2  27681  nofulllem4  27693  altxpsspw  27855  hfuni  28069  fin2so  28260  mbfresfi  28282  mbfposadd  28283  cnambfre  28284  itg2addnclem2  28288  ibladdnclem  28292  itgaddnclem1  28294  iblabsnclem  28299  iblmulc2nc  28301  itggt0cn  28308  ftc1cnnclem  28309  ftc1anclem3  28313  ftc1anclem5  28315  ftc1anclem8  28318  ftc1anc  28319  locfindis  28421  tailf  28440  tailfb  28442  supex2g  28475  sdclem1  28483  constcncf  28502  sub1cncf  28504  sub2cncf  28505  sstotbnd2  28517  equivbnd2  28535  ismtyres  28551  rrnheibor  28580  reheibor  28582  iccbnd  28583  icccmpALT  28584  exidres  28587  exidresid  28588  mzpnegmpt  28925  vdioph  28963  3anrabdioph  28966  3orrabdioph  28967  rexrabdioph  28977  rexfrabdioph  28978  2rexfrabdioph  28979  3rexfrabdioph  28980  4rexfrabdioph  28981  6rexfrabdioph  28982  7rexfrabdioph  28983  elnnrabdioph  28990  dvdsrabdioph  28993  eldioph4b  28995  pellfundgt1  29069  jm2.27c  29201  lsmfgcl  29272  lmhmfgima  29282  lmhmlnmsplit  29285  pwssplit4  29287  pwslnm  29292  areaquad  29437  sblpnf  29441  fsumcnf  29588  refsum2cnlem1  29604  fmulcl  29607  itgsin0pilem1  29636  itgsinexplem1  29640  stoweidlem2  29643  stoweidlem3  29644  stoweidlem5  29646  stoweidlem16  29657  stoweidlem18  29659  stoweidlem20  29661  stoweidlem21  29662  stoweidlem22  29663  stoweidlem23  29664  stoweidlem31  29672  stoweidlem32  29673  stoweidlem35  29676  stoweidlem36  29677  stoweidlem40  29681  stoweidlem41  29682  stoweidlem47  29688  stoweidlem50  29691  stoweidlem57  29698  stoweidlem59  29700  stoweidlem60  29701  stoweidlem62  29703  wallispi2lem2  29713  el2xptp0  29973  otel3xp  29974  fsumz  30082  fsummsndifre  30083  fsummmodsndifre  30085  fsummsnunz  30087  fsummmodsnunre  30089  qerclwwlknfi  30349  hashclwwlkn0  30350  hashwwlkext  30411  frgrawopreglem1  30483  mptcfsupp  30624  linply1  30635  lincext1  30697  lincext2  30698  lindslinindimp2lem1  30701  lincresunit1  30720  lincresunit2  30721  dp2cl  30813  bnj893  31623  bnj944  31633  bnj969  31641  bnj1136  31690  bnj1177  31699  bnj1452  31745  bnj1489  31749  bj-snglex  32049  bj-projex  32071  bj-pr1ex  32082  bj-1uplex  32084  bj-pr2ex  32096  bj-2uplex  32098  lshpinN  32207  dalemdea  32879  dalem5  32884  dalem8  32887  dalem9  32889  dalem15  32895  dalem23  32913  cdlemblem  33010  osumcllem1N  33173  osumcllem9N  33181  pexmidlem6N  33192  lhpat2  33262  arglem1N  33407  cdleme0aa  33427  cdleme1b  33443  cdleme1  33444  cdleme2  33445  cdleme3b  33446  cdleme3e  33449  cdleme3h  33452  cdleme7b  33461  cdleme7e  33464  cdleme7ga  33465  cdleme9b  33469  cdleme15d  33494  cdleme22gb  33511  cdlemedb  33514  cdlemeda  33515  cdleme23b  33567  cdleme25cl  33574  cdleme27cl  33583  cdleme29cl  33594  cdlemefs27cl  33630  cdleme42c  33689  cdleme42h  33699  cdleme42i  33700  cdlemg4c  33829  cdlemg4  33834  cdlemg6c  33837  cdlemkvcl  34059  cdlemkoatnle  34068  cdlemk14  34071  cdlemk15  34072  cdlemk29-3  34128  cdlemk37  34131  dia2dimlem1  34282  dvheveccl  34330  diblss  34388  dihglblem5  34516  dih1dimatlem  34547  dihat  34553  dihjatcclem1  34636  dihjatcclem2  34637  dihjatcclem4  34639  dochexmidlem5  34682  dochexmidlem6  34683  lclkrlem2m  34737  lclkrlem2o  34739  lcfrlem3  34762  lcfrlem22  34782  lcfrlem25  34785  lcfrlem30  34790  lcfrlem37  34797  mapdpglem17N  34906  mapdpglem19  34908  hdmap1val  35017
  Copyright terms: Public domain W3C validator