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

Theorem syl5eqel 2488
Description: B 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 2478 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:  syl5eqelr  2489  csbexg  3221  snex  4365  dmresexg  5128  f1oabexg  5645  cofunexg  5918  cofunex2g  5919  abrexex2g  5947  fovrn  6175  fnovrn  6180  xpexgALT  6256  fnwelem  6420  opiota  6494  riotaprop  6532  tfrlem12  6609  rdgseg  6639  oelim2  6797  oeeulem  6803  ecexg  6868  qsexg  6921  pmex  6982  resixpfo  7059  elixpsn  7060  unxpdomlem3  7274  rabfi  7292  fnfi  7343  rnfi  7350  iunfi  7353  unifi  7354  suppfif1  7358  pwfilem  7359  supexd  7414  oemapvali  7596  mapfien  7609  wemapwe  7610  cnfcomlem  7612  cnfcom  7613  cnfcom2lem  7614  cnfcom2  7615  cnfcom3lem  7616  cnfcom3  7617  prwf  7693  scott0  7766  htalem  7776  infxpenlem  7851  dfac8b  7868  cfss  8101  cofsmo  8105  coftr  8109  fin1a2lem10  8245  hsmexlem4  8265  hsmex2  8269  fpwwe  8477  canthwelem  8481  pwfseqlem1  8489  wuntp  8542  wunsn  8547  wunsuc  8548  wunr1om  8550  wunot  8554  r1limwun  8567  tsk1  8595  tsk2  8596  tskr1om  8598  gruuni  8631  grusn  8635  gruina  8649  wuncn  9001  negcl  9262  peano5nni  9959  peano5uzi  10314  quoremz  11191  quoremnn0  11192  quoremnn0ALT  11193  intfrac2  11194  intfracq  11195  seqf1olem1  11317  seqf1olem2  11318  serle  11333  discr1  11470  cats1cld  11774  sqrlem4  12006  sqreulem  12118  reccn2  12345  fsump1i  12508  fsumabs  12535  o1fsum  12547  supcvg  12590  mertenslem1  12616  mertenslem2  12617  rpnnen2  12780  ruclem12  12795  bitsfzolem  12901  bezoutlem2  12994  algrf  13019  algcvg  13022  algcvga  13025  algfx  13026  eucalgcvga  13032  eucalg  13033  prmdiv  13129  pythagtriplem11  13154  pythagtriplem13  13156  pcprecl  13168  infpnlem1  13233  infpnlem2  13234  4sqlem5  13265  mul4sqlem  13276  4sqlem13  13280  4sqlem14  13281  4sqlem17  13284  4sqlem18  13285  vdwlem5  13308  wunndx  13440  wunress  13483  restid  13616  mreexdomd  13829  acsfn0  13840  acsfn1  13841  acsfn2  13843  funcf2  14020  funcpropd  14052  fthepi  14080  ressffth  14090  elhomai2  14144  catcxpccl  14259  diag1cl  14294  yonedalem1  14324  spwex  14616  prdsinvlem  14881  subggrp  14902  nsgacs  14931  ghmima  14981  gimco  15010  gicref  15013  cayley  15067  cntrnsg  15095  oppgmnd  15105  efgredlemf  15328  efgredlemd  15331  efgredlemc  15332  cycsubgcyg  15465  gsumzaddlem  15481  gsum2d  15501  dprdfid  15530  dprd2dlem1  15554  dprd2da  15555  ablfacrplem  15578  ablfacrp  15579  ablfacrp2  15580  ablfac1lem  15581  pgpfac1lem1  15587  pgpfac1lem2  15588  pgpfac1lem3a  15589  pgpfac1lem3  15590  pgpfac1lem4  15591  pgpfac1lem5  15592  pgpfaclem1  15594  ablfaclem3  15600  opprrng  15691  subrgrng  15826  lmhmkerlss  16082  rlmlmod  16231  lidl0cl  16238  lidlacl  16239  lidlnegcl  16240  lidlmcl  16243  lidlacs  16247  fidomndrnglem  16321  gsumbagdiag  16396  psrass1lem  16397  mplsubrglem  16457  evlslem2  16523  vr1cl2  16546  vr1cl  16566  subrgvr1cl  16610  zlpirlem2  16724  zlpirlem3  16725  cygznlem1  16802  cygznlem2a  16803  cygznlem3  16805  isphld  16840  topopn  16934  rintopn  16937  fctop  17023  topcld  17054  intcld  17059  uncld  17060  unicld  17065  mretopd  17111  neiptoptop  17150  tgrest  17177  restin  17184  neitr  17198  restcls  17199  restntr  17200  restlp  17201  restperf  17202  perfopn  17203  ordtbaslem  17206  ordtuni  17208  ordtbas2  17209  ordtbas  17210  ordttopon  17211  ordtopn1  17212  ordtopn2  17213  ordtrest2lem  17221  ordtrest2  17222  cnco  17284  cnrest  17303  cnprest2  17308  lmss  17316  cncmp  17409  imacmp  17414  fiuncmp  17421  concompcon  17448  cldllycmp  17511  hausmapdom  17516  kgentopon  17523  1stckgen  17539  ptbasin  17562  ptbasfi  17566  pttopon  17581  xkotopon  17585  txbasval  17591  ptpjcn  17596  ptcldmpt  17599  dfac14lem  17602  txcn  17611  ptcn  17612  ptrescn  17624  txkgen  17637  cnmpt12f  17651  xkofvcn  17669  qtopval2  17681  elqtop  17682  qtoptop2  17684  hmeoco  17757  idhmeo  17758  ordthmeolem  17786  ptunhmeo  17793  xkohmeo  17800  qtopf1  17801  cfinfil  17878  ufprim  17894  ufildr  17916  fin1aufil  17917  fmfg  17934  elfm3  17935  fbflim  17961  flimclslem  17969  flffbas  17980  cnpflf2  17985  flfcnp2  17992  fclsbas  18006  alexsublem  18028  ptcmplem3  18038  ptcmpg  18041  cnextcn  18051  tgpsubcn  18073  tmdgsum  18078  symgtgp  18084  tmdlactcn  18085  submtmd  18087  clssubg  18091  divstgplem  18103  prdstmdd  18106  tsmsfbas  18110  eltsms  18115  tsmssubm  18125  dvrcn  18166  utop2nei  18233  utop3cls  18234  utopreg  18235  blres  18414  prdsbl  18474  metrest  18507  metustexhalfOLD  18546  metustexhalf  18547  subgngp  18629  nlmvscnlem2  18674  nlmvscnlem1  18675  nrginvrcnlem  18679  qtopbaslem  18745  tgqioo  18784  icccmplem2  18807  icccmp  18809  reconnlem2  18811  xrge0tsms  18818  nmcn  18828  metnrmlem2  18843  divcn  18851  fsumcn  18853  fsum2cn  18854  cncfmet  18891  addccncf  18899  cnmpt2pc  18906  icchmeo  18919  cnrehmeo  18931  cnheiborlem  18932  bndth  18936  lebnumlem2  18940  htpycom  18954  htpyid  18955  htpyco1  18956  htpycc  18958  reparphti  18975  pcohtpylem  18997  pcoptcl  18999  pcoass  19002  pcorevcl  19003  pcorevlem  19004  ipcnlem2  19151  ipcnlem1  19152  cmsss  19256  minveclem4c  19279  minveclem3b  19282  minveclem4a  19284  minveclem4  19286  minveclem6  19288  pjthlem1  19291  ivthlem2  19302  ivthlem3  19303  ovolicc2lem4  19369  finiunmbl  19391  voliunlem1  19397  ioombl1lem1  19405  ioombl1lem3  19407  ioombl1lem4  19408  ovolioo  19415  opnmblALT  19448  mbfimaicc  19478  mbfid  19481  mbfeqalem  19487  mbfres  19489  cncombf  19503  mbfi1flim  19568  itg2monolem2  19596  itg2monolem3  19597  itg2mono  19598  itg2cnlem1  19606  itgcl  19628  iblss  19649  itgeqa  19658  itgss3  19659  itgless  19661  iblconst  19662  ibladdlem  19664  itgaddlem1  19667  iblabslem  19672  iblabsr  19674  iblmulc2  19675  itggt0  19686  itgcn  19687  limcvallem  19711  limcflflem  19720  limcres  19726  cnplimc  19727  limccnp  19731  limccnp2  19732  dvreslem  19749  dvres2lem  19750  dvcnp  19758  dvnff  19762  dvmptres2  19801  dvmptres  19802  dvmptntr  19810  dvmptfsum  19812  dvcnvlem  19813  dvcnv  19814  dvferm1lem  19821  dvferm2lem  19823  dvlipcn  19831  dvlip2  19832  c1liplem1  19833  lhop1lem  19850  dvcnvrelem2  19855  dvcvx  19857  dvfsumge  19859  dvfsumlem3  19865  ftc1lem3  19875  ftc1lem4  19876  evl1rhm  19902  ply1remlem  20038  ply0  20080  plyid  20081  plyeq0lem  20082  dgrub  20106  dgrub2  20107  dgrlb  20108  coeidlem  20109  coeaddlem  20120  coemullem  20121  coemulhi  20125  dgreq0  20136  dgrlt  20137  dgradd2  20139  dgrmul  20141  dgrcolem2  20145  dgrco  20146  plycj  20148  coecj  20149  plydivlem2  20164  plydivlem4  20166  plyremlem  20174  plyrem  20175  quotcan  20179  vieta1lem1  20180  elqaalem2  20190  elqaalem3  20191  radcnvcl  20286  psercnlem1  20294  pserdvlem2  20297  pilem2  20321  pilem3  20322  logfac  20448  logcnlem2  20487  logcnlem3  20488  logcnlem4  20489  dvlog  20495  cxpcn  20582  cxpcn3lem  20584  ang180lem1  20604  ang180lem2  20605  ang180lem3  20606  pythag  20612  quart1lem  20648  xrlimcnp  20760  efrlim  20761  ftalem1  20808  ftalem2  20809  ftalem4  20811  ftalem5  20812  basellem1  20816  basellem2  20817  basellem3  20818  basellem4  20819  basellem5  20820  basellem8  20823  dchr1cl  20988  dchrinvcl  20990  dchrptlem1  21001  dchrptlem2  21002  bposlem3  21023  bposlem5  21025  bposlem6  21026  lgsqrlem2  21079  lgsqrlem3  21080  lgsqrlem4  21081  lgseisenlem1  21086  lgseisenlem2  21087  lgseisenlem3  21088  lgseisenlem4  21089  lgsquadlem1  21091  lgsquadlem2  21092  lgsquadlem3  21093  2sqlem8  21109  chebbnd1lem1  21116  chebbnd1lem2  21117  chebbnd1lem3  21118  mulog2sumlem2  21182  selberglem2  21193  chpdifbndlem1  21200  chpdifbndlem2  21201  pntrmax  21211  pntpbnd1a  21232  pntpbnd1  21233  pntpbnd2  21234  pntibndlem1  21236  pntibndlem2  21238  pntibndlem3  21239  pntlemd  21241  pntlemc  21242  pntlema  21243  pntlemg  21245  pntlemr  21249  pntlemj  21250  ostth2lem2  21281  ostth2lem3  21282  ostth2lem4  21283  ostth2  21284  ostth3  21285  usgrares1  21377  usgrafilem2  21379  cusgraexilem1  21428  cusgrares  21434  cusgrasizeinds  21438  cusgrafilem3  21443  wlks  21479  trls  21489  grpoinvfval  21765  grpodivfval  21783  gxfval  21798  ghgrp  21909  isvc  22013  isnv  22044  imsmet  22136  smcnlem  22146  minvecolem2  22330  minvecolem3  22331  minvecolem4c  22334  minvecolem4  22335  minvecolem5  22336  minvecolem6  22337  hhssabloi  22715  pjhthlem1  22846  pjoc1i  22886  cnlnadjlem3  23525  cnlnadjlem5  23527  mdsymlem1  23859  mdsymlem3  23861  abrexexd  23943  elovimad  24004  xrge0pluscn  24279  prsiga  24467  inelsiga  24471  mbfmcst  24562  mbfmco  24567  mbfmcnt  24571  dya2icoseg  24580  sibf0  24602  sibff  24604  sibfof  24607  sitgclg  24609  0rrv  24662  rrvsum  24665  erdsze2lem1  24842  erdsze2lem2  24843  txsconlem  24880  cvxpcon  24882  cvxscon  24883  cvmsiota  24917  cvmliftiota  24941  cvmlift2lem10  24952  ghomgrp  25054  nobndlem2  25561  nofulllem4  25573  altxpsspw  25726  eleesub  25754  axsegconlem2  25761  axsegconlem8  25767  axlowdimlem7  25791  axlowdimlem17  25801  hfuni  26029  mbfresfi  26152  mbfposadd  26153  cnambfre  26154  itg2addnclem2  26156  ibladdnclem  26160  itgaddnclem1  26162  iblabsnclem  26167  iblmulc2nc  26169  itggt0cn  26176  ftc1cnnclem  26177  locfindis  26275  tailf  26294  tailfb  26296  supex2g  26329  sdclem1  26337  constcncf  26358  sub1cncf  26360  sub2cncf  26361  sstotbnd2  26373  equivbnd2  26391  ismtyres  26407  rrnheibor  26436  reheibor  26438  iccbnd  26439  icccmpALT  26440  exidres  26443  exidresid  26444  mzpnegmpt  26691  vdioph  26728  3anrabdioph  26731  3orrabdioph  26732  rexrabdioph  26744  rexfrabdioph  26745  2rexfrabdioph  26746  3rexfrabdioph  26747  4rexfrabdioph  26748  6rexfrabdioph  26749  7rexfrabdioph  26750  elnnrabdioph  26757  dvdsrabdioph  26760  eldioph4b  26762  pellfundgt1  26836  jm2.27c  26968  lsmfgcl  27040  lmhmfgima  27050  lmhmlnmsplit  27053  pwssplit4  27059  pwslnm  27064  uvcff  27108  frlmsplit2  27111  lindsmm  27166  psgndmsubg  27293  sblpnf  27407  fsumcnf  27559  refsum2cnlem1  27575  fmulcl  27578  itgsin0pilem1  27611  itgsinexplem1  27615  stoweidlem2  27618  stoweidlem3  27619  stoweidlem5  27621  stoweidlem16  27632  stoweidlem18  27634  stoweidlem20  27636  stoweidlem21  27637  stoweidlem22  27638  stoweidlem23  27639  stoweidlem31  27647  stoweidlem32  27648  stoweidlem35  27651  stoweidlem36  27652  stoweidlem40  27656  stoweidlem41  27657  stoweidlem47  27663  stoweidlem50  27666  stoweidlem57  27673  stoweidlem59  27675  stoweidlem60  27676  stoweidlem62  27678  wallispi2lem2  27688  el2xptp0  27949  otel3xp  27950  swrdccatin12lem1  28019  swrdccat3a  28030  swrdccat3b  28031  frgrawopreglem1  28147  dp2cl  28226  bnj893  29005  bnj944  29015  bnj969  29023  bnj1136  29072  bnj1177  29081  bnj1452  29127  bnj1489  29131  lshpinN  29472  dalemdea  30144  dalem5  30149  dalem8  30152  dalem9  30154  dalem15  30160  dalem23  30178  cdlemblem  30275  osumcllem1N  30438  osumcllem9N  30446  pexmidlem6N  30457  lhpat2  30527  arglem1N  30672  cdleme0aa  30692  cdleme1b  30708  cdleme1  30709  cdleme2  30710  cdleme3b  30711  cdleme3e  30714  cdleme3h  30717  cdleme7b  30726  cdleme7e  30729  cdleme7ga  30730  cdleme9b  30734  cdleme15d  30759  cdleme22gb  30776  cdlemedb  30779  cdlemeda  30780  cdleme23b  30832  cdleme25cl  30839  cdleme27cl  30848  cdleme29cl  30859  cdlemefs27cl  30895  cdleme42c  30954  cdleme42h  30964  cdleme42i  30965  cdlemg4c  31094  cdlemg4  31099  cdlemg6c  31102  cdlemkvcl  31324  cdlemkoatnle  31333  cdlemk14  31336  cdlemk15  31337  cdlemk29-3  31393  cdlemk37  31396  dia2dimlem1  31547  dvheveccl  31595  diblss  31653  dihglblem5  31781  dih1dimatlem  31812  dihat  31818  dihjatcclem1  31901  dihjatcclem2  31902  dihjatcclem4  31904  dochexmidlem5  31947  dochexmidlem6  31948  lclkrlem2m  32002  lclkrlem2o  32004  lcfrlem3  32027  lcfrlem22  32047  lcfrlem25  32050  lcfrlem30  32055  lcfrlem37  32062  mapdpglem17N  32171  mapdpglem19  32173  hdmap1val  32282
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