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

Theorem syl5eqel 2522
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 2512 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    e. wcel 1756
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-cleq 2431  df-clel 2434
This theorem is referenced by:  syl5eqelr  2523  csbexg  4419  csbexgOLD  4421  rabexd  4439  snex  4528  dmresexg  5128  riotaprop  6071  fovrn  6228  fnovrn  6233  ovima0  6237  f1oabexg  6531  cofunexg  6536  cofunex2g  6537  abrexex2g  6549  xpexgALT  6565  opiota  6628  fnwelem  6682  mptsuppdifd  6706  tfrlem12  6840  rdgseg  6870  oelim2  7026  oeeulem  7032  ecexg  7097  qsexg  7150  pmex  7211  resixpfo  7293  elixpsn  7294  unxpdomlem3  7511  rabfi  7529  fnfi  7581  rnfi  7588  iunfi  7591  unifi  7592  pwfilem  7597  fsuppun  7631  fsuppcolem  7642  mapfienlem2  7647  supexd  7695  cantnfp1lem1  7878  oemapvali  7884  mapfienOLD  7919  wemapwe  7920  wemapweOLD  7921  cnfcomlem  7924  cnfcom  7925  cnfcom2lem  7926  cnfcom2  7927  cnfcom3lem  7928  cnfcom3  7929  cnfcomlemOLD  7932  cnfcomOLD  7933  cnfcom2lemOLD  7934  cnfcom2OLD  7935  cnfcom3lemOLD  7936  cnfcom3OLD  7937  prwf  8010  scott0  8085  htalem  8095  infxpenlem  8172  dfac8b  8193  cfss  8426  cofsmo  8430  coftr  8434  fin1a2lem10  8570  hsmexlem4  8590  hsmex2  8594  fpwwe  8805  canthwelem  8809  pwfseqlem1  8817  wuntp  8870  wunsn  8875  wunsuc  8876  wunr1om  8878  wunot  8882  r1limwun  8895  tsk1  8923  tsk2  8924  tskr1om  8926  gruuni  8959  grusn  8963  gruina  8977  wuncn  9329  negcl  9602  peano5nni  10317  peano5uzi  10722  quoremz  11686  quoremnn0  11687  quoremnn0ALT  11688  intfrac2  11689  intfracq  11690  seqf1olem1  11837  seqf1olem2  11838  serle  11853  discr1  11992  swrdccatin2  12370  swrdccatin12lem2  12372  swrdccatin12  12374  swrdccat3  12375  swrdccat3a  12377  cats1cld  12474  sqrlem4  12727  sqreulem  12839  reccn2  13066  fsump1i  13228  fsumabs  13256  o1fsum  13268  supcvg  13310  mertenslem1  13336  mertenslem2  13337  rpnnen2  13500  ruclem12  13515  bitsfzolem  13622  bezoutlem2  13715  algrf  13740  algcvg  13743  algcvga  13746  algfx  13747  eucalgcvga  13753  eucalg  13754  prmdiv  13852  pythagtriplem11  13884  pythagtriplem13  13886  pcprecl  13898  infpnlem1  13963  infpnlem2  13964  4sqlem5  13995  mul4sqlem  14006  4sqlem13  14010  4sqlem14  14011  4sqlem17  14014  4sqlem18  14015  vdwlem5  14038  wunndx  14182  wunress  14229  restid  14364  mreexdomd  14579  acsfn0  14590  acsfn1  14591  acsfn2  14593  funcf2  14770  funcpropd  14802  fthepi  14830  ressffth  14840  elhomai2  14894  catcxpccl  15009  diag1cl  15044  yonedalem1  15074  prdsinvlem  15654  subggrp  15675  nsgacs  15708  ghmima  15758  gimco  15787  gicref  15790  cntrnsg  15850  oppgmnd  15860  cayley  15910  symgfixfolem1  15935  pmtrdifellem1  15973  psgndmsubg  15999  efgredlemf  16229  efgredlemd  16232  efgredlemc  16233  cycsubgcyg  16368  gsumzaddlem  16399  gsumzaddlemOLD  16401  gsum2dlem1  16449  gsum2dlem2  16450  gsum2dOLD  16452  dprdfid  16495  dprdfidOLD  16502  dprd2dlem1  16528  dprd2da  16529  ablfacrplem  16554  ablfacrp  16555  ablfacrp2  16556  ablfac1lem  16557  pgpfac1lem1  16563  pgpfac1lem2  16564  pgpfac1lem3a  16565  pgpfac1lem3  16566  pgpfac1lem4  16567  pgpfac1lem5  16568  pgpfaclem1  16570  ablfaclem3  16576  opprrng  16711  subrgrng  16846  lmhmkerlss  17109  rlmlmod  17263  lidl0cl  17271  lidlacl  17272  lidlnegcl  17273  lidlmcl  17276  lidlacs  17280  fidomndrnglem  17355  gsumbagdiag  17423  psrass1lem  17424  psrlidm  17451  psrridm  17453  mplsubrglem  17494  mplsubrglemOLD  17495  vr1cl2  17624  vr1cl  17646  subrgvr1cl  17691  evl1rhm  17741  evl1gsumdlem  17765  zringlpirlem2  17879  zringlpirlem3  17880  zlpirlem2  17884  zlpirlem3  17885  cygznlem1  17974  cygznlem2a  17975  cygznlem3  17977  isphld  18058  lindsmm  18232  1marepvmarrepid  18361  1marepvsma1  18369  mdetleib2  18374  smadiadetlem3  18449  cramerimplem1  18464  cramerimplem2  18465  cramerimplem3  18466  cramerimp  18467  topopn  18494  rintopn  18497  fctop  18583  topcld  18614  intcld  18619  uncld  18620  unicld  18625  mretopd  18671  neiptoptop  18710  tgrest  18738  restin  18745  neitr  18759  restcls  18760  restntr  18761  restlp  18762  restperf  18763  perfopn  18764  ordtbaslem  18767  ordtuni  18769  ordtbas2  18770  ordtbas  18771  ordttopon  18772  ordtopn1  18773  ordtopn2  18774  ordtrest2lem  18782  ordtrest2  18783  cnco  18845  cnrest  18864  cnprest2  18869  lmss  18877  cncmp  18970  imacmp  18975  fiuncmp  18982  bwthOLD  18989  concompcon  19011  cldllycmp  19074  hausmapdom  19079  kgentopon  19086  1stckgen  19102  ptbasin  19125  ptbasfi  19129  pttopon  19144  xkotopon  19148  txbasval  19154  ptpjcn  19159  ptcldmpt  19162  dfac14lem  19165  txcn  19174  ptcn  19175  ptrescn  19187  txkgen  19200  cnmpt12f  19214  xkofvcn  19232  qtopval2  19244  elqtop  19245  qtoptop2  19247  hmeoco  19320  idhmeo  19321  ordthmeolem  19349  ptunhmeo  19356  xkohmeo  19363  qtopf1  19364  cfinfil  19441  ufprim  19457  ufildr  19479  fin1aufil  19480  fmfg  19497  elfm3  19498  fbflim  19524  flimclslem  19532  flffbas  19543  cnpflf2  19548  flfcnp2  19555  fclsbas  19569  alexsublem  19591  ptcmplem3  19601  ptcmpg  19604  cnextcn  19614  tgpsubcn  19636  tmdgsum  19641  symgtgp  19647  tmdlactcn  19648  submtmd  19650  clssubg  19654  divstgplem  19666  prdstmdd  19669  tsmsfbas  19673  eltsms  19678  tsmssubm  19691  dvrcn  19733  utop2nei  19800  utop3cls  19801  utopreg  19802  blres  19981  prdsbl  20041  metrest  20074  metustexhalfOLD  20113  metustexhalf  20114  subgngp  20196  nlmvscnlem2  20241  nlmvscnlem1  20242  nrginvrcnlem  20246  qtopbaslem  20312  tgqioo  20352  icccmplem2  20375  icccmp  20377  reconnlem2  20379  xrge0tsms  20386  nmcn  20396  metnrmlem2  20411  divcn  20419  fsumcn  20421  fsum2cn  20422  cncfmet  20459  addccncf  20467  cnmpt2pc  20475  icchmeo  20488  cnrehmeo  20500  cnheiborlem  20501  bndth  20505  lebnumlem2  20509  htpycom  20523  htpyid  20524  htpyco1  20525  htpycc  20527  reparphti  20544  pcohtpylem  20566  pcoptcl  20568  pcoass  20571  pcorevcl  20572  pcorevlem  20573  ipcnlem2  20731  ipcnlem1  20732  cmsss  20836  minveclem4c  20887  minveclem3b  20890  minveclem4a  20892  minveclem4  20894  minveclem6  20896  pjthlem1  20899  ivthlem2  20911  ivthlem3  20912  ovolicc2lem4  20978  finiunmbl  21000  voliunlem1  21006  ioombl1lem1  21014  ioombl1lem3  21016  ioombl1lem4  21017  ovolioo  21024  opnmblALT  21058  mbfimaicc  21086  mbfid  21089  mbfeqalem  21095  mbfres  21097  cncombf  21111  mbfi1flim  21176  itg2monolem2  21204  itg2monolem3  21205  itg2mono  21206  itg2cnlem1  21214  itgcl  21236  iblss  21257  itgeqa  21266  itgss3  21267  itgless  21269  iblconst  21270  ibladdlem  21272  itgaddlem1  21275  iblabslem  21280  iblabsr  21282  iblmulc2  21283  itggt0  21294  itgcn  21295  limcvallem  21321  limcflflem  21330  limcres  21336  cnplimc  21337  limccnp  21341  limccnp2  21342  dvreslem  21359  dvres2lem  21360  dvcnp  21368  dvnff  21372  dvmptres2  21411  dvmptres  21412  dvmptntr  21420  dvmptfsum  21422  dvcnvlem  21423  dvcnv  21424  dvferm1lem  21431  dvferm2lem  21433  dvlipcn  21441  dvlip2  21442  c1liplem1  21443  lhop1lem  21460  dvcnvrelem2  21465  dvcvx  21467  dvfsumge  21469  dvfsumlem3  21475  ftc1lem3  21485  ftc1lem4  21486  mdegleb  21510  ply1remlem  21609  ply0  21651  plyid  21652  plyeq0lem  21653  dgrub  21677  dgrub2  21678  dgrlb  21679  coeidlem  21680  coeaddlem  21691  coemullem  21692  coemulhi  21696  dgreq0  21707  dgrlt  21708  dgradd2  21710  dgrmul  21712  dgrcolem2  21716  dgrco  21717  plycj  21719  coecj  21720  plydivlem2  21735  plydivlem4  21737  plyremlem  21745  plyrem  21746  quotcan  21750  vieta1lem1  21751  elqaalem2  21761  elqaalem3  21762  radcnvcl  21857  psercnlem1  21865  pserdvlem2  21868  pilem2  21892  pilem3  21893  logfac  22024  logcnlem2  22063  logcnlem3  22064  logcnlem4  22065  dvlog  22071  cxpcn  22158  cxpcn3lem  22160  ang180lem1  22180  ang180lem2  22181  ang180lem3  22182  pythag  22188  heron  22208  quart1lem  22225  xrlimcnp  22337  efrlim  22338  ftalem1  22385  ftalem2  22386  ftalem4  22388  ftalem5  22389  basellem1  22393  basellem2  22394  basellem3  22395  basellem4  22396  basellem5  22397  basellem8  22400  dchr1cl  22565  dchrinvcl  22567  dchrptlem1  22578  dchrptlem2  22579  bposlem3  22600  bposlem5  22602  bposlem6  22603  lgsqrlem2  22656  lgsqrlem3  22657  lgsqrlem4  22658  lgseisenlem1  22663  lgseisenlem2  22664  lgseisenlem3  22665  lgseisenlem4  22666  lgsquadlem1  22668  lgsquadlem2  22669  lgsquadlem3  22670  2sqlem8  22686  chebbnd1lem1  22693  chebbnd1lem2  22694  chebbnd1lem3  22695  mulog2sumlem2  22759  selberglem2  22770  chpdifbndlem1  22777  chpdifbndlem2  22778  pntrmax  22788  pntpbnd1a  22809  pntpbnd1  22810  pntpbnd2  22811  pntibndlem1  22813  pntibndlem2  22815  pntibndlem3  22816  pntlemd  22818  pntlemc  22819  pntlema  22820  pntlemg  22822  pntlemr  22826  pntlemj  22827  ostth2lem2  22858  ostth2lem3  22859  ostth2lem4  22860  ostth2  22861  ostth3  22862  tgelrnln  23006  mirauto  23043  eleesub  23108  axsegconlem2  23115  axsegconlem8  23121  axlowdimlem7  23145  axlowdimlem17  23155  usgrares1  23274  usgrafilem2  23276  cusgraexilem1  23325  cusgrares  23331  cusgrasizeinds  23335  cusgrafilem3  23340  wlks  23376  trls  23386  grpoinvfval  23662  grpodivfval  23680  gxfval  23695  ghgrp  23806  isvc  23910  isnv  23941  imsmet  24033  smcnlem  24043  minvecolem2  24227  minvecolem3  24228  minvecolem4c  24231  minvecolem4  24232  minvecolem5  24233  minvecolem6  24234  hhssabloi  24614  pjhthlem1  24745  pjoc1i  24785  cnlnadjlem3  25424  cnlnadjlem5  25426  mdsymlem1  25758  mdsymlem3  25760  abrexexd  25841  elovimad  25907  gsumle  26197  gsummpt2co  26200  ordtconlem1  26306  xrge0pluscn  26322  prsiga  26526  inelsiga  26530  mbfmcst  26626  mbfmco  26631  mbfmcnt  26635  dya2icoseg  26644  sibf0  26672  sibff  26674  sibfinima  26677  sibfof  26678  sitgclg  26680  eulerpartlemt  26706  sseqval  26723  0rrv  26786  rrvsum  26789  signsplypnf  26903  signsply0  26904  signsvtn0  26923  signstfveq0a  26929  signstfveq0  26930  signsvtp  26936  signsvtn  26937  signsvfpn  26938  signsvfnn  26939  erdsze2lem1  27043  erdsze2lem2  27044  txsconlem  27081  cvxpcon  27083  cvxscon  27084  cvmsiota  27118  cvmliftiota  27142  cvmlift2lem10  27153  ghomgrp  27260  wsucex  27714  wsuccl  27715  nobndlem2  27785  nofulllem4  27797  altxpsspw  27959  hfuni  28173  fin2so  28369  mbfresfi  28391  mbfposadd  28392  cnambfre  28393  itg2addnclem2  28397  ibladdnclem  28401  itgaddnclem1  28403  iblabsnclem  28408  iblmulc2nc  28410  itggt0cn  28417  ftc1cnnclem  28418  ftc1anclem3  28422  ftc1anclem5  28424  ftc1anclem8  28427  ftc1anc  28428  locfindis  28530  tailf  28549  tailfb  28551  supex2g  28584  sdclem1  28592  constcncf  28611  sub1cncf  28613  sub2cncf  28614  sstotbnd2  28626  equivbnd2  28644  ismtyres  28660  rrnheibor  28689  reheibor  28691  iccbnd  28692  icccmpALT  28693  exidres  28696  exidresid  28697  mzpnegmpt  29033  vdioph  29071  3anrabdioph  29074  3orrabdioph  29075  rexrabdioph  29085  rexfrabdioph  29086  2rexfrabdioph  29087  3rexfrabdioph  29088  4rexfrabdioph  29089  6rexfrabdioph  29090  7rexfrabdioph  29091  elnnrabdioph  29098  dvdsrabdioph  29101  eldioph4b  29103  pellfundgt1  29177  jm2.27c  29309  lsmfgcl  29380  lmhmfgima  29390  lmhmlnmsplit  29393  pwssplit4  29395  pwslnm  29400  areaquad  29545  sblpnf  29549  fsumcnf  29696  refsum2cnlem1  29712  fmulcl  29715  itgsin0pilem1  29743  itgsinexplem1  29747  stoweidlem2  29750  stoweidlem3  29751  stoweidlem5  29753  stoweidlem16  29764  stoweidlem18  29766  stoweidlem20  29768  stoweidlem21  29769  stoweidlem22  29770  stoweidlem23  29771  stoweidlem31  29779  stoweidlem32  29780  stoweidlem35  29783  stoweidlem36  29784  stoweidlem40  29788  stoweidlem41  29789  stoweidlem47  29795  stoweidlem50  29798  stoweidlem57  29805  stoweidlem59  29807  stoweidlem60  29808  stoweidlem62  29810  wallispi2lem2  29820  el2xptp0  30080  otel3xp  30081  fsumz  30189  fsummsndifre  30190  fsummmodsndifre  30192  fsummsnunz  30194  fsummmodsnunre  30196  qerclwwlknfi  30456  hashclwwlkn0  30457  hashwwlkext  30518  frgrawopreglem1  30590  mptcfsupp  30744  fsuppmapnn0fiublem  30747  fsuppmapnn0fiub  30748  linply1  30776  lincext1  30877  lincext2  30878  lindslinindimp2lem1  30881  lincresunit1  30900  lincresunit2  30901  dp2cl  30993  bnj893  31808  bnj944  31818  bnj969  31826  bnj1136  31875  bnj1177  31884  bnj1452  31930  bnj1489  31934  bj-snglex  32313  bj-projex  32335  bj-pr1ex  32346  bj-1uplex  32348  bj-pr2ex  32360  bj-2uplex  32362  lshpinN  32474  dalemdea  33146  dalem5  33151  dalem8  33154  dalem9  33156  dalem15  33162  dalem23  33180  cdlemblem  33277  osumcllem1N  33440  osumcllem9N  33448  pexmidlem6N  33459  lhpat2  33529  arglem1N  33674  cdleme0aa  33694  cdleme1b  33710  cdleme1  33711  cdleme2  33712  cdleme3b  33713  cdleme3e  33716  cdleme3h  33719  cdleme7b  33728  cdleme7e  33731  cdleme7ga  33732  cdleme9b  33736  cdleme15d  33761  cdleme22gb  33778  cdlemedb  33781  cdlemeda  33782  cdleme23b  33834  cdleme25cl  33841  cdleme27cl  33850  cdleme29cl  33861  cdlemefs27cl  33897  cdleme42c  33956  cdleme42h  33966  cdleme42i  33967  cdlemg4c  34096  cdlemg4  34101  cdlemg6c  34104  cdlemkvcl  34326  cdlemkoatnle  34335  cdlemk14  34338  cdlemk15  34339  cdlemk29-3  34395  cdlemk37  34398  dia2dimlem1  34549  dvheveccl  34597  diblss  34655  dihglblem5  34783  dih1dimatlem  34814  dihat  34820  dihjatcclem1  34903  dihjatcclem2  34904  dihjatcclem4  34906  dochexmidlem5  34949  dochexmidlem6  34950  lclkrlem2m  35004  lclkrlem2o  35006  lcfrlem3  35029  lcfrlem22  35049  lcfrlem25  35052  lcfrlem30  35057  lcfrlem37  35064  mapdpglem17N  35173  mapdpglem19  35175  hdmap1val  35284
  Copyright terms: Public domain W3C validator