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

Theorem syl5eqel 2494
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 2490 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1405    e. wcel 1842
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1634  df-cleq 2394  df-clel 2397
This theorem is referenced by:  syl5eqelr  2495  3eltr4g  2508  csbexg  4527  rabexd  4545  snex  4631  otel3xp  4978  dmresexg  5237  riotaprop  6219  elovimad  6274  fovrn  6382  fnovrn  6387  ovima0  6391  f1oabexg  6697  cofunexg  6702  cofunex2g  6703  abrexex2g  6715  xpexgALT  6731  el2xptp0  6782  opiota  6797  fnwelem  6853  mptsuppdifd  6879  fvmpt2curryd  6957  tfrlem12  7015  rdgseg  7045  oelim2  7201  oeeulem  7207  ecexg  7272  qsexg  7326  pmex  7382  resixpfo  7465  elixpsn  7466  unxpdomlem3  7681  rabfi  7699  fnfi  7752  rnfi  7759  iunfi  7762  unifi  7763  pwfilem  7768  fsuppun  7802  fsuppcolem  7814  mapfienlem2  7819  supexd  7866  cantnfp1lem1  8049  oemapvali  8055  mapfienOLD  8090  wemapwe  8091  wemapweOLD  8092  cnfcomlem  8095  cnfcom  8096  cnfcom2lem  8097  cnfcom2  8098  cnfcom3lem  8099  cnfcom3  8100  cnfcomlemOLD  8103  cnfcomOLD  8104  cnfcom2lemOLD  8105  cnfcom2OLD  8106  cnfcom3lemOLD  8107  cnfcom3OLD  8108  prwf  8181  scott0  8256  htalem  8266  infxpenlem  8343  dfac8b  8364  cfss  8597  cofsmo  8601  coftr  8605  fin1a2lem10  8741  hsmexlem4  8761  hsmex2  8765  fpwwe  8974  canthwelem  8978  pwfseqlem1  8986  wuntp  9039  wunsn  9044  wunsuc  9045  wunr1om  9047  wunot  9051  r1limwun  9064  tsk1  9092  tsk2  9093  tskr1om  9095  gruuni  9128  grusn  9132  gruina  9146  wuncn  9497  negcl  9776  peano5nni  10499  peano5uzi  10912  quoremz  11933  quoremnn0  11934  quoremnn0ALT  11935  intfrac2  11936  intfracq  11937  fsuppmapnn0fiublem  12050  fsuppmapnn0fiub  12051  seqf1olem1  12100  seqf1olem2  12101  serle  12116  discr1  12256  swrdccatin2  12675  swrdccatin12lem2  12677  swrdccatin12  12679  swrdccat3  12680  swrdccat3a  12682  cats1cld  12783  sqrlem4  13135  sqreulem  13248  reccn2  13475  fsumzcl2  13616  fsummsnunz  13627  fsump1i  13642  fsumabs  13673  o1fsum  13685  supcvg  13726  mertenslem1  13752  mertenslem2  13753  rpnnen2  14060  ruclem12  14075  bitsfzolem  14185  bezoutlem2  14278  algrf  14303  algcvg  14306  algcvga  14309  algfx  14310  eucalgcvga  14316  eucalg  14317  prmdiv  14416  pythagtriplem11  14450  pythagtriplem13  14452  pcprecl  14464  infpnlem1  14529  infpnlem2  14530  4sqlem5  14561  mul4sqlem  14572  4sqlem13  14576  4sqlem14  14577  4sqlem17  14580  4sqlem18  14581  vdwlem5  14604  wunndx  14749  wunress  14800  1strwunbndx  14839  restid  14940  mreexdomd  15155  acsfn0  15166  acsfn1  15167  acsfn2  15169  rcaninv  15299  funcf2  15373  funcpropd  15405  fthepi  15433  ressffth  15443  elhomai2  15529  catcxpccl  15692  diag1cl  15727  yonedalem1  15757  prdsinvlem  16394  subggrp  16420  nsgacs  16453  ghmima  16503  gimco  16532  gicref  16535  cntrnsg  16595  oppgmnd  16605  cayley  16655  symgfixfolem1  16679  pmtrdifellem1  16717  psgndmsubg  16743  efgredlemf  16975  efgredlemd  16978  efgredlemc  16979  cycsubgcyg  17119  gsumzaddlem  17150  gsumzaddlemOLD  17152  gsum2dlem1  17210  gsum2dlem2  17211  gsum2dOLD  17213  dprdfid  17269  dprdfidOLD  17276  dprd2dlem1  17302  dprd2da  17303  ablfacrplem  17328  ablfacrp  17329  ablfacrp2  17330  ablfac1lem  17331  pgpfac1lem1  17337  pgpfac1lem2  17338  pgpfac1lem3a  17339  pgpfac1lem3  17340  pgpfac1lem4  17341  pgpfac1lem5  17342  pgpfaclem1  17344  ablfaclem3  17350  opprring  17492  subrgring  17644  lmhmkerlss  17909  rlmlmod  18063  lidl0cl  18071  lidlacl  18072  lidlnegcl  18073  lidlmcl  18077  lidlacs  18081  fidomndrnglem  18167  gsumbagdiag  18240  psrass1lem  18241  psrlidm  18268  psrridm  18270  mplsubrglem  18312  mplsubrglemOLD  18313  vr1cl2  18444  vr1cl  18470  subrgvr1cl  18515  coe1fzgsumdlem  18555  evl1rhm  18580  evl1gsumdlem  18604  zringlpirlem2  18715  zringlpirlem3  18716  cygznlem1  18795  cygznlem2a  18796  cygznlem3  18798  isphld  18879  lindsmm  19047  mpt2matmul  19132  scmatscmiddistr  19194  scmatf  19215  1marepvmarrepid  19261  1marepvsma1  19269  mdetleib2  19274  smadiadetlem3  19354  cramerimplem1  19369  cramerimplem2  19370  cramerimplem3  19371  cramerimp  19372  pmatcollpwscmatlem2  19475  pmatcollpwscmat  19476  mp2pm2mplem4  19494  chmatcl  19513  cpmidgsum  19553  cpmidgsumm2pm  19554  cpmidpmatlem2  19556  cpmidpmatlem3  19557  chcoeffeqlem  19570  cayhamlem3  19572  topopn  19599  rintopn  19602  fctop  19689  topcld  19720  intcld  19725  uncld  19726  unicld  19731  mretopd  19778  neiptoptop  19817  tgrest  19845  restin  19852  neitr  19866  restcls  19867  restntr  19868  restlp  19869  restperf  19870  perfopn  19871  ordtbaslem  19874  ordtuni  19876  ordtbas2  19877  ordtbas  19878  ordttopon  19879  ordtopn1  19880  ordtopn2  19881  ordtrest2lem  19889  ordtrest2  19890  cnco  19952  cnrest  19971  cnprest2  19976  lmss  19984  cncmp  20077  imacmp  20082  fiuncmp  20089  concompcon  20117  cldllycmp  20180  hausmapdom  20185  lfinun  20210  locfindis  20215  kgentopon  20223  1stckgen  20239  ptbasin  20262  ptbasfi  20266  pttopon  20281  xkotopon  20285  txbasval  20291  ptpjcn  20296  ptcldmpt  20299  dfac14lem  20302  txcn  20311  ptcn  20312  ptrescn  20324  txkgen  20337  cnmpt12f  20351  xkofvcn  20369  qtopval2  20381  elqtop  20382  qtoptop2  20384  hmeoco  20457  idhmeo  20458  ordthmeolem  20486  ptunhmeo  20493  xkohmeo  20500  qtopf1  20501  cfinfil  20578  ufprim  20594  ufildr  20616  fin1aufil  20617  fmfg  20634  elfm3  20635  fbflim  20661  flimclslem  20669  flffbas  20680  cnpflf2  20685  flfcnp2  20692  fclsbas  20706  alexsublem  20728  ptcmplem3  20738  ptcmpg  20741  cnextcn  20751  tgpsubcn  20773  tmdgsum  20778  symgtgp  20784  tmdlactcn  20785  submtmd  20787  clssubg  20791  qustgplem  20803  prdstmdd  20806  tsmsfbas  20810  eltsms  20815  tsmssubm  20828  dvrcn  20870  utop2nei  20937  utop3cls  20938  utopreg  20939  blres  21118  prdsbl  21178  metrest  21211  metustexhalfOLD  21250  metustexhalf  21251  subgngp  21333  nlmvscnlem2  21378  nlmvscnlem1  21379  nrginvrcnlem  21383  qtopbaslem  21449  tgqioo  21489  icccmplem2  21512  icccmp  21514  reconnlem2  21516  xrge0tsms  21523  nmcn  21533  metnrmlem2  21548  divcn  21556  fsumcn  21558  fsum2cn  21559  cncfmet  21596  addccncf  21604  cnmpt2pc  21612  icchmeo  21625  cnrehmeo  21637  cnheiborlem  21638  bndth  21642  lebnumlem2  21646  htpycom  21660  htpyid  21661  htpyco1  21662  htpycc  21664  reparphti  21681  pcohtpylem  21703  pcoptcl  21705  pcoass  21708  pcorevcl  21709  pcorevlem  21710  ipcnlem2  21868  ipcnlem1  21869  cmsss  21973  minveclem4c  22024  minveclem3b  22027  minveclem4a  22029  minveclem4  22031  minveclem6  22033  pjthlem1  22036  ivthlem2  22048  ivthlem3  22049  ovolicc2lem4  22115  finiunmbl  22138  voliunlem1  22144  ioombl1lem1  22152  ioombl1lem3  22154  ioombl1lem4  22155  ovolioo  22162  opnmblALT  22196  mbfimaicc  22224  mbfid  22227  mbfeqalem  22233  mbfres  22235  cncombf  22249  mbfi1flim  22314  itg2monolem2  22342  itg2monolem3  22343  itg2mono  22344  itg2cnlem1  22352  itgcl  22374  iblss  22395  itgeqa  22404  itgss3  22405  itgless  22407  iblconst  22408  ibladdlem  22410  itgaddlem1  22413  iblabslem  22418  iblabsr  22420  iblmulc2  22421  itggt0  22432  itgcn  22433  limcvallem  22459  limcflflem  22468  limcres  22474  cnplimc  22475  limccnp  22479  limccnp2  22480  dvreslem  22497  dvres2lem  22498  dvcnp  22506  dvnff  22510  dvmptres2  22549  dvmptres  22550  dvmptntr  22558  dvmptfsum  22560  dvcnvlem  22561  dvcnv  22562  dvferm1lem  22569  dvferm2lem  22571  dvlipcn  22579  dvlip2  22580  c1liplem1  22581  lhop1lem  22598  dvcnvrelem2  22603  dvcvx  22605  dvfsumge  22607  dvfsumlem3  22613  ftc1lem3  22623  ftc1lem4  22624  mdegleb  22648  ply1remlem  22747  ply0  22789  plyid  22790  plyeq0lem  22791  dgrub  22815  dgrub2  22816  dgrlb  22817  coeidlem  22818  coeaddlem  22830  coemullem  22831  coemulhi  22835  dgreq0  22846  dgrlt  22847  dgradd2  22849  dgrmul  22851  dgrcolem2  22855  dgrco  22856  plycj  22858  coecj  22859  plydivlem2  22874  plydivlem4  22876  plyremlem  22884  plyrem  22885  quotcan  22889  vieta1lem1  22890  elqaalem2  22900  elqaalem3  22901  radcnvcl  22996  psercnlem1  23004  pserdvlem2  23007  pilem2  23031  pilem3  23032  efabl  23121  efsubm  23122  logfac  23172  logcnlem2  23210  logcnlem3  23211  logcnlem4  23212  dvlog  23218  cxpcn  23307  cxpcn3lem  23309  ang180lem1  23360  ang180lem2  23361  ang180lem3  23362  pythag  23368  heron  23386  quart1lem  23403  xrlimcnp  23516  efrlim  23517  ftalem1  23619  ftalem2  23620  ftalem4  23622  ftalem5  23623  basellem1  23627  basellem2  23628  basellem3  23629  basellem4  23630  basellem5  23631  basellem8  23634  dchr1cl  23799  dchrinvcl  23801  dchrptlem1  23812  dchrptlem2  23813  bposlem3  23834  bposlem5  23836  bposlem6  23837  lgsqrlem2  23890  lgsqrlem3  23891  lgsqrlem4  23892  lgseisenlem1  23897  lgseisenlem2  23898  lgseisenlem3  23899  lgseisenlem4  23900  lgsquadlem1  23902  lgsquadlem2  23903  lgsquadlem3  23904  2sqlem8  23920  chebbnd1lem1  23927  chebbnd1lem2  23928  chebbnd1lem3  23929  mulog2sumlem2  23993  selberglem2  24004  chpdifbndlem1  24011  chpdifbndlem2  24012  pntrmax  24022  pntpbnd1a  24043  pntpbnd1  24044  pntpbnd2  24045  pntibndlem1  24047  pntibndlem2  24049  pntibndlem3  24050  pntlemd  24052  pntlemc  24053  pntlema  24054  pntlemg  24056  pntlemr  24060  pntlemj  24061  ostth2lem2  24092  ostth2lem3  24093  ostth2lem4  24094  ostth2  24095  ostth3  24096  tgelrnln  24287  mirauto  24338  lmiisolem  24438  eleesub  24512  axsegconlem2  24519  axsegconlem8  24525  axlowdimlem7  24549  axlowdimlem17  24559  usgrares1  24708  usgrafilem2  24710  cusgrares  24770  cusgrasizeinds  24774  cusgrafilem3  24779  wlks  24817  trls  24836  hashwwlkext  25044  qerclwwlknfi  25127  hashclwwlkn0  25128  frgrawopreglem1  25342  grpoinvfval  25520  grpodivfval  25538  gxfval  25553  ghgrpOLD  25664  isvc  25768  isnv  25799  imsmet  25891  smcnlem  25901  minvecolem2  26085  minvecolem3  26086  minvecolem4c  26089  minvecolem4  26090  minvecolem5  26091  minvecolem6  26092  hhssabloi  26472  pjhthlem1  26603  pjoc1i  26643  cnlnadjlem3  27281  cnlnadjlem5  27283  mdsymlem1  27615  mdsymlem3  27617  abrexexd  27702  acunirnmpt  27823  acunirnmpt2  27824  acunirnmpt2f  27825  aciunf1lem  27826  imafi2  27853  gsumle  28101  gsummpt2co  28102  ordtconlem1  28239  xrge0pluscn  28255  prsiga  28459  inelsiga  28463  sigapildsys  28490  ldgenpisyslem1  28491  ldgenpisys  28494  inelros  28501  fiunelros  28502  mbfmcst  28587  mbfmco  28592  mbfmcnt  28596  dya2icoseg  28605  fiunelcarsg  28644  carsggect  28646  omsmeas  28651  sibf0  28662  sibff  28664  sibfinima  28667  sibfof  28668  sitgclg  28670  eulerpartlemt  28696  sseqval  28713  0rrv  28776  rrvsum  28779  signsplypnf  28893  signsply0  28894  signsvtn0  28913  signstfveq0a  28919  signstfveq0  28920  signsvtp  28926  signsvtn  28927  signsvfpn  28928  signsvfnn  28929  bnj893  29194  bnj944  29204  bnj969  29212  bnj1136  29261  bnj1177  29270  bnj1452  29316  bnj1489  29320  erdsze2lem1  29381  erdsze2lem2  29382  txsconlem  29418  cvxpcon  29420  cvxscon  29421  cvmsiota  29455  cvmliftiota  29479  cvmlift2lem10  29490  ghomgrp  29763  wsucex  30055  wsuccl  30056  nobndlem2  30126  nofulllem4  30138  altxpsspw  30288  hfuni  30510  tailf  30591  tailfb  30593  bj-snglex  31084  bj-projex  31106  bj-pr1ex  31117  bj-1uplex  31119  bj-pr2ex  31131  bj-2uplex  31133  fin2so  31393  mbfresfi  31414  mbfposadd  31415  cnambfre  31416  itg2addnclem2  31421  ibladdnclem  31425  itgaddnclem1  31427  iblabsnclem  31432  iblmulc2nc  31434  itggt0cn  31441  ftc1cnnclem  31442  ftc1anclem3  31446  ftc1anclem5  31448  ftc1anclem8  31451  ftc1anc  31452  supex2g  31491  sdclem1  31499  constcncf  31518  sub1cncf  31520  sub2cncf  31521  sstotbnd2  31533  equivbnd2  31551  ismtyres  31567  rrnheibor  31596  reheibor  31598  iccbnd  31599  icccmpALT  31600  exidres  31603  exidresid  31604  lshpinN  31988  dalemdea  32660  dalem5  32665  dalem8  32668  dalem9  32670  dalem15  32676  dalem23  32694  cdlemblem  32791  osumcllem1N  32954  osumcllem9N  32962  pexmidlem6N  32973  lhpat2  33043  arglem1N  33189  cdleme0aa  33209  cdleme1b  33225  cdleme1  33226  cdleme2  33227  cdleme3b  33228  cdleme3e  33231  cdleme3h  33234  cdleme7b  33243  cdleme7e  33246  cdleme7ga  33247  cdleme9b  33251  cdleme15d  33276  cdleme22gb  33293  cdlemedb  33296  cdlemeda  33297  cdleme23b  33350  cdleme25cl  33357  cdleme27cl  33366  cdleme29cl  33377  cdlemefs27cl  33413  cdleme42c  33472  cdleme42h  33482  cdleme42i  33483  cdlemg4c  33612  cdlemg4  33617  cdlemg6c  33620  cdlemkvcl  33842  cdlemkoatnle  33851  cdlemk14  33854  cdlemk15  33855  cdlemk29-3  33911  cdlemk37  33914  dia2dimlem1  34065  dvheveccl  34113  diblss  34171  dihglblem5  34299  dih1dimatlem  34330  dihat  34336  dihjatcclem1  34419  dihjatcclem2  34420  dihjatcclem4  34422  dochexmidlem5  34465  dochexmidlem6  34466  lclkrlem2m  34520  lclkrlem2o  34522  lcfrlem3  34545  lcfrlem22  34565  lcfrlem25  34568  lcfrlem30  34573  lcfrlem37  34580  mapdpglem17N  34689  mapdpglem19  34691  hdmap1val  34800  mzpnegmpt  35019  vdioph  35055  3anrabdioph  35058  3orrabdioph  35059  rexrabdioph  35070  rexfrabdioph  35071  2rexfrabdioph  35072  3rexfrabdioph  35073  4rexfrabdioph  35074  6rexfrabdioph  35075  7rexfrabdioph  35076  elnnrabdioph  35083  dvdsrabdioph  35086  eldioph4b  35087  pellfundgt1  35161  jm2.27c  35292  lsmfgcl  35363  lmhmfgima  35373  lmhmlnmsplit  35376  pwssplit4  35378  pwslnm  35383  areaquad  35529  sblpnf  36019  fsumcnf  36757  rnmptfi  36803  suprnmpt  36807  fzisoeu  36850  upbdrech  36855  upbdrech2  36858  fmulcl  36925  fprodcllemf  36941  ellimciota  36970  constlimc  36980  sumnnodd  36986  addccncf2  37028  cncfiooicclem1  37046  dvresntr  37063  ioodvbdlimc1lem1  37078  ioodvbdlimc1lem2  37079  ioodvbdlimc2lem  37081  dvnmul  37090  itgsin0pilem1  37098  itgsinexplem1  37102  mbfres2cn  37107  iblsplit  37115  iblsplitf  37119  stoweidlem2  37134  stoweidlem3  37135  stoweidlem5  37137  stoweidlem16  37148  stoweidlem18  37150  stoweidlem20  37152  stoweidlem21  37153  stoweidlem22  37154  stoweidlem23  37155  stoweidlem31  37163  stoweidlem32  37164  stoweidlem36  37168  stoweidlem40  37172  stoweidlem41  37173  stoweidlem47  37179  stoweidlem50  37182  stoweidlem57  37189  stoweidlem59  37191  stoweidlem60  37192  stoweidlem62  37194  wallispi2lem2  37204  dirkertrigeqlem1  37230  dirkeritg  37234  dirkercncflem1  37235  dirkercncflem4  37238  fourierdlem4  37243  fourierdlem6  37245  fourierdlem7  37246  fourierdlem19  37258  fourierdlem20  37259  fourierdlem25  37264  fourierdlem26  37265  fourierdlem30  37269  fourierdlem31  37270  fourierdlem32  37271  fourierdlem33  37272  fourierdlem35  37274  fourierdlem36  37275  fourierdlem41  37280  fourierdlem42  37281  fourierdlem47  37286  fourierdlem48  37287  fourierdlem49  37288  fourierdlem50  37289  fourierdlem51  37290  fourierdlem52  37291  fourierdlem54  37293  fourierdlem62  37301  fourierdlem63  37302  fourierdlem64  37303  fourierdlem65  37304  fourierdlem71  37310  fourierdlem76  37315  fourierdlem79  37318  fourierdlem80  37319  fourierdlem85  37324  fourierdlem86  37325  fourierdlem87  37326  fourierdlem89  37328  fourierdlem90  37329  fourierdlem91  37330  fourierdlem94  37333  fourierdlem97  37336  fourierdlem102  37341  fourierdlem103  37342  fourierdlem104  37343  fourierdlem107  37346  fourierdlem113  37352  fourierdlem114  37353  fourierswlem  37363  fouriersw  37364  elaa2lem  37366  etransclem23  37390  etransclem43  37410  etransclem45  37412  etransclem46  37413  etransclem47  37414  etransclem48  37415  iccpartigtl  37670  3odd  37768  4even  37769  5odd  37770  bgoldbtbndlem2  37834  bgoldbtbndlem3  37835  pfxccatin12lem2  37891  pfxccatin12  37892  pfxccat3  37893  pfxccatpfx2  37895  pfxccat3a  37896  fsummsndifre  37954  fsummmodsndifre  37956  fsummmodsnunz  37957  usgrafisbaseALT  38049  usgrafisbaseALT2  38050  usgfislem2  38054  usgfisALTlem2  38058  rnghmsscmap2  38272  rhmsscmap2  38318  rhmsscrnghm  38325  fldc  38382  fldhmsubc  38383  fldcALTV  38401  fldhmsubcALTV  38402  mptcfsupp  38464  linply1  38484  lincext1  38546  lincext2  38547  lindslinindimp2lem1  38550  lincresunit1  38569  lincresunit2  38570  fllogbd  38671  dp2cl  38789  aacllem  38840
  Copyright terms: Public domain W3C validator