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

Theorem syl5eqel 2519
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 2509 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    e. wcel 1725
This theorem is referenced by:  syl5eqelr  2520  csbexg  3253  snex  4397  dmresexg  5160  f1oabexg  5677  cofunexg  5950  cofunex2g  5951  abrexex2g  5979  fovrn  6207  fnovrn  6212  xpexgALT  6288  fnwelem  6452  opiota  6526  riotaprop  6564  tfrlem12  6641  rdgseg  6671  oelim2  6829  oeeulem  6835  ecexg  6900  qsexg  6953  pmex  7014  resixpfo  7091  elixpsn  7092  unxpdomlem3  7306  rabfi  7324  fnfi  7375  rnfi  7382  iunfi  7385  unifi  7386  suppfif1  7391  pwfilem  7392  supexd  7447  oemapvali  7629  mapfien  7642  wemapwe  7643  cnfcomlem  7645  cnfcom  7646  cnfcom2lem  7647  cnfcom2  7648  cnfcom3lem  7649  cnfcom3  7650  prwf  7726  scott0  7799  htalem  7809  infxpenlem  7884  dfac8b  7901  cfss  8134  cofsmo  8138  coftr  8142  fin1a2lem10  8278  hsmexlem4  8298  hsmex2  8302  fpwwe  8510  canthwelem  8514  pwfseqlem1  8522  wuntp  8575  wunsn  8580  wunsuc  8581  wunr1om  8583  wunot  8587  r1limwun  8600  tsk1  8628  tsk2  8629  tskr1om  8631  gruuni  8664  grusn  8668  gruina  8682  wuncn  9034  negcl  9295  peano5nni  9992  peano5uzi  10347  quoremz  11224  quoremnn0  11225  quoremnn0ALT  11226  intfrac2  11227  intfracq  11228  seqf1olem1  11350  seqf1olem2  11351  serle  11366  discr1  11503  cats1cld  11807  sqrlem4  12039  sqreulem  12151  reccn2  12378  fsump1i  12541  fsumabs  12568  o1fsum  12580  supcvg  12623  mertenslem1  12649  mertenslem2  12650  rpnnen2  12813  ruclem12  12828  bitsfzolem  12934  bezoutlem2  13027  algrf  13052  algcvg  13055  algcvga  13058  algfx  13059  eucalgcvga  13065  eucalg  13066  prmdiv  13162  pythagtriplem11  13187  pythagtriplem13  13189  pcprecl  13201  infpnlem1  13266  infpnlem2  13267  4sqlem5  13298  mul4sqlem  13309  4sqlem13  13313  4sqlem14  13314  4sqlem17  13317  4sqlem18  13318  vdwlem5  13341  wunndx  13473  wunress  13516  restid  13649  mreexdomd  13862  acsfn0  13873  acsfn1  13874  acsfn2  13876  funcf2  14053  funcpropd  14085  fthepi  14113  ressffth  14123  elhomai2  14177  catcxpccl  14292  diag1cl  14327  yonedalem1  14357  spwex  14649  prdsinvlem  14914  subggrp  14935  nsgacs  14964  ghmima  15014  gimco  15043  gicref  15046  cayley  15100  cntrnsg  15128  oppgmnd  15138  efgredlemf  15361  efgredlemd  15364  efgredlemc  15365  cycsubgcyg  15498  gsumzaddlem  15514  gsum2d  15534  dprdfid  15563  dprd2dlem1  15587  dprd2da  15588  ablfacrplem  15611  ablfacrp  15612  ablfacrp2  15613  ablfac1lem  15614  pgpfac1lem1  15620  pgpfac1lem2  15621  pgpfac1lem3a  15622  pgpfac1lem3  15623  pgpfac1lem4  15624  pgpfac1lem5  15625  pgpfaclem1  15627  ablfaclem3  15633  opprrng  15724  subrgrng  15859  lmhmkerlss  16115  rlmlmod  16264  lidl0cl  16271  lidlacl  16272  lidlnegcl  16273  lidlmcl  16276  lidlacs  16280  fidomndrnglem  16354  gsumbagdiag  16429  psrass1lem  16430  mplsubrglem  16490  evlslem2  16556  vr1cl2  16579  vr1cl  16599  subrgvr1cl  16643  zlpirlem2  16757  zlpirlem3  16758  cygznlem1  16835  cygznlem2a  16836  cygznlem3  16838  isphld  16873  topopn  16967  rintopn  16970  fctop  17056  topcld  17087  intcld  17092  uncld  17093  unicld  17098  mretopd  17144  neiptoptop  17183  tgrest  17211  restin  17218  neitr  17232  restcls  17233  restntr  17234  restlp  17235  restperf  17236  perfopn  17237  ordtbaslem  17240  ordtuni  17242  ordtbas2  17243  ordtbas  17244  ordttopon  17245  ordtopn1  17246  ordtopn2  17247  ordtrest2lem  17255  ordtrest2  17256  cnco  17318  cnrest  17337  cnprest2  17342  lmss  17350  cncmp  17443  imacmp  17448  fiuncmp  17455  bwth  17461  concompcon  17483  cldllycmp  17546  hausmapdom  17551  kgentopon  17558  1stckgen  17574  ptbasin  17597  ptbasfi  17601  pttopon  17616  xkotopon  17620  txbasval  17626  ptpjcn  17631  ptcldmpt  17634  dfac14lem  17637  txcn  17646  ptcn  17647  ptrescn  17659  txkgen  17672  cnmpt12f  17686  xkofvcn  17704  qtopval2  17716  elqtop  17717  qtoptop2  17719  hmeoco  17792  idhmeo  17793  ordthmeolem  17821  ptunhmeo  17828  xkohmeo  17835  qtopf1  17836  cfinfil  17913  ufprim  17929  ufildr  17951  fin1aufil  17952  fmfg  17969  elfm3  17970  fbflim  17996  flimclslem  18004  flffbas  18015  cnpflf2  18020  flfcnp2  18027  fclsbas  18041  alexsublem  18063  ptcmplem3  18073  ptcmpg  18076  cnextcn  18086  tgpsubcn  18108  tmdgsum  18113  symgtgp  18119  tmdlactcn  18120  submtmd  18122  clssubg  18126  divstgplem  18138  prdstmdd  18141  tsmsfbas  18145  eltsms  18150  tsmssubm  18160  dvrcn  18201  utop2nei  18268  utop3cls  18269  utopreg  18270  blres  18449  prdsbl  18509  metrest  18542  metustexhalfOLD  18581  metustexhalf  18582  subgngp  18664  nlmvscnlem2  18709  nlmvscnlem1  18710  nrginvrcnlem  18714  qtopbaslem  18780  tgqioo  18819  icccmplem2  18842  icccmp  18844  reconnlem2  18846  xrge0tsms  18853  nmcn  18863  metnrmlem2  18878  divcn  18886  fsumcn  18888  fsum2cn  18889  cncfmet  18926  addccncf  18934  cnmpt2pc  18941  icchmeo  18954  cnrehmeo  18966  cnheiborlem  18967  bndth  18971  lebnumlem2  18975  htpycom  18989  htpyid  18990  htpyco1  18991  htpycc  18993  reparphti  19010  pcohtpylem  19032  pcoptcl  19034  pcoass  19037  pcorevcl  19038  pcorevlem  19039  ipcnlem2  19186  ipcnlem1  19187  cmsss  19291  minveclem4c  19314  minveclem3b  19317  minveclem4a  19319  minveclem4  19321  minveclem6  19323  pjthlem1  19326  ivthlem2  19337  ivthlem3  19338  ovolicc2lem4  19404  finiunmbl  19426  voliunlem1  19432  ioombl1lem1  19440  ioombl1lem3  19442  ioombl1lem4  19443  ovolioo  19450  opnmblALT  19483  mbfimaicc  19513  mbfid  19516  mbfeqalem  19522  mbfres  19524  cncombf  19538  mbfi1flim  19603  itg2monolem2  19631  itg2monolem3  19632  itg2mono  19633  itg2cnlem1  19641  itgcl  19663  iblss  19684  itgeqa  19693  itgss3  19694  itgless  19696  iblconst  19697  ibladdlem  19699  itgaddlem1  19702  iblabslem  19707  iblabsr  19709  iblmulc2  19710  itggt0  19721  itgcn  19722  limcvallem  19746  limcflflem  19755  limcres  19761  cnplimc  19762  limccnp  19766  limccnp2  19767  dvreslem  19784  dvres2lem  19785  dvcnp  19793  dvnff  19797  dvmptres2  19836  dvmptres  19837  dvmptntr  19845  dvmptfsum  19847  dvcnvlem  19848  dvcnv  19849  dvferm1lem  19856  dvferm2lem  19858  dvlipcn  19866  dvlip2  19867  c1liplem1  19868  lhop1lem  19885  dvcnvrelem2  19890  dvcvx  19892  dvfsumge  19894  dvfsumlem3  19900  ftc1lem3  19910  ftc1lem4  19911  evl1rhm  19937  ply1remlem  20073  ply0  20115  plyid  20116  plyeq0lem  20117  dgrub  20141  dgrub2  20142  dgrlb  20143  coeidlem  20144  coeaddlem  20155  coemullem  20156  coemulhi  20160  dgreq0  20171  dgrlt  20172  dgradd2  20174  dgrmul  20176  dgrcolem2  20180  dgrco  20181  plycj  20183  coecj  20184  plydivlem2  20199  plydivlem4  20201  plyremlem  20209  plyrem  20210  quotcan  20214  vieta1lem1  20215  elqaalem2  20225  elqaalem3  20226  radcnvcl  20321  psercnlem1  20329  pserdvlem2  20332  pilem2  20356  pilem3  20357  logfac  20483  logcnlem2  20522  logcnlem3  20523  logcnlem4  20524  dvlog  20530  cxpcn  20617  cxpcn3lem  20619  ang180lem1  20639  ang180lem2  20640  ang180lem3  20641  pythag  20647  quart1lem  20683  xrlimcnp  20795  efrlim  20796  ftalem1  20843  ftalem2  20844  ftalem4  20846  ftalem5  20847  basellem1  20851  basellem2  20852  basellem3  20853  basellem4  20854  basellem5  20855  basellem8  20858  dchr1cl  21023  dchrinvcl  21025  dchrptlem1  21036  dchrptlem2  21037  bposlem3  21058  bposlem5  21060  bposlem6  21061  lgsqrlem2  21114  lgsqrlem3  21115  lgsqrlem4  21116  lgseisenlem1  21121  lgseisenlem2  21122  lgseisenlem3  21123  lgseisenlem4  21124  lgsquadlem1  21126  lgsquadlem2  21127  lgsquadlem3  21128  2sqlem8  21144  chebbnd1lem1  21151  chebbnd1lem2  21152  chebbnd1lem3  21153  mulog2sumlem2  21217  selberglem2  21228  chpdifbndlem1  21235  chpdifbndlem2  21236  pntrmax  21246  pntpbnd1a  21267  pntpbnd1  21268  pntpbnd2  21269  pntibndlem1  21271  pntibndlem2  21273  pntibndlem3  21274  pntlemd  21276  pntlemc  21277  pntlema  21278  pntlemg  21280  pntlemr  21284  pntlemj  21285  ostth2lem2  21316  ostth2lem3  21317  ostth2lem4  21318  ostth2  21319  ostth3  21320  usgrares1  21412  usgrafilem2  21414  cusgraexilem1  21463  cusgrares  21469  cusgrasizeinds  21473  cusgrafilem3  21478  wlks  21514  trls  21524  grpoinvfval  21800  grpodivfval  21818  gxfval  21833  ghgrp  21944  isvc  22048  isnv  22079  imsmet  22171  smcnlem  22181  minvecolem2  22365  minvecolem3  22366  minvecolem4c  22369  minvecolem4  22370  minvecolem5  22371  minvecolem6  22372  hhssabloi  22750  pjhthlem1  22881  pjoc1i  22921  cnlnadjlem3  23560  cnlnadjlem5  23562  mdsymlem1  23894  mdsymlem3  23896  abrexexd  23978  elovimad  24039  xrge0pluscn  24314  prsiga  24502  inelsiga  24506  mbfmcst  24597  mbfmco  24602  mbfmcnt  24606  dya2icoseg  24615  sibf0  24637  sibff  24639  sibfof  24642  sitgclg  24644  0rrv  24697  rrvsum  24700  erdsze2lem1  24877  erdsze2lem2  24878  txsconlem  24915  cvxpcon  24917  cvxscon  24918  cvmsiota  24952  cvmliftiota  24976  cvmlift2lem10  24987  ghomgrp  25089  nobndlem2  25602  nofulllem4  25614  altxpsspw  25770  eleesub  25798  axsegconlem2  25805  axsegconlem8  25811  axlowdimlem7  25835  axlowdimlem17  25845  hfuni  26073  mbfresfi  26199  mbfposadd  26200  cnambfre  26201  itg2addnclem2  26203  ibladdnclem  26207  itgaddnclem1  26209  iblabsnclem  26214  iblmulc2nc  26216  itggt0cn  26223  ftc1cnnclem  26224  locfindis  26322  tailf  26341  tailfb  26343  supex2g  26376  sdclem1  26384  constcncf  26405  sub1cncf  26407  sub2cncf  26408  sstotbnd2  26420  equivbnd2  26438  ismtyres  26454  rrnheibor  26483  reheibor  26485  iccbnd  26486  icccmpALT  26487  exidres  26490  exidresid  26491  mzpnegmpt  26738  vdioph  26775  3anrabdioph  26778  3orrabdioph  26779  rexrabdioph  26791  rexfrabdioph  26792  2rexfrabdioph  26793  3rexfrabdioph  26794  4rexfrabdioph  26795  6rexfrabdioph  26796  7rexfrabdioph  26797  elnnrabdioph  26804  dvdsrabdioph  26807  eldioph4b  26809  pellfundgt1  26883  jm2.27c  27015  lsmfgcl  27087  lmhmfgima  27097  lmhmlnmsplit  27100  pwssplit4  27106  pwslnm  27111  uvcff  27155  frlmsplit2  27158  lindsmm  27213  psgndmsubg  27340  sblpnf  27454  fsumcnf  27606  refsum2cnlem1  27622  fmulcl  27625  itgsin0pilem1  27658  itgsinexplem1  27662  stoweidlem2  27665  stoweidlem3  27666  stoweidlem5  27668  stoweidlem16  27679  stoweidlem18  27681  stoweidlem20  27683  stoweidlem21  27684  stoweidlem22  27685  stoweidlem23  27686  stoweidlem31  27694  stoweidlem32  27695  stoweidlem35  27698  stoweidlem36  27699  stoweidlem40  27703  stoweidlem41  27704  stoweidlem47  27710  stoweidlem50  27713  stoweidlem57  27720  stoweidlem59  27722  stoweidlem60  27723  stoweidlem62  27725  wallispi2lem2  27735  el2xptp0  27997  otel3xp  27998  swrdccatin12lem1  28094  swrdccat3a  28105  swrdccat3b  28106  shwrdssizesame  28171  frgrawopreglem1  28291  dp2cl  28370  bnj893  29153  bnj944  29163  bnj969  29171  bnj1136  29220  bnj1177  29229  bnj1452  29275  bnj1489  29279  lshpinN  29626  dalemdea  30298  dalem5  30303  dalem8  30306  dalem9  30308  dalem15  30314  dalem23  30332  cdlemblem  30429  osumcllem1N  30592  osumcllem9N  30600  pexmidlem6N  30611  lhpat2  30681  arglem1N  30826  cdleme0aa  30846  cdleme1b  30862  cdleme1  30863  cdleme2  30864  cdleme3b  30865  cdleme3e  30868  cdleme3h  30871  cdleme7b  30880  cdleme7e  30883  cdleme7ga  30884  cdleme9b  30888  cdleme15d  30913  cdleme22gb  30930  cdlemedb  30933  cdlemeda  30934  cdleme23b  30986  cdleme25cl  30993  cdleme27cl  31002  cdleme29cl  31013  cdlemefs27cl  31049  cdleme42c  31108  cdleme42h  31118  cdleme42i  31119  cdlemg4c  31248  cdlemg4  31253  cdlemg6c  31256  cdlemkvcl  31478  cdlemkoatnle  31487  cdlemk14  31490  cdlemk15  31491  cdlemk29-3  31547  cdlemk37  31550  dia2dimlem1  31701  dvheveccl  31749  diblss  31807  dihglblem5  31935  dih1dimatlem  31966  dihat  31972  dihjatcclem1  32055  dihjatcclem2  32056  dihjatcclem4  32058  dochexmidlem5  32101  dochexmidlem6  32102  lclkrlem2m  32156  lclkrlem2o  32158  lcfrlem3  32181  lcfrlem22  32201  lcfrlem25  32204  lcfrlem30  32209  lcfrlem37  32216  mapdpglem17N  32325  mapdpglem19  32327  hdmap1val  32436
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-cleq 2428  df-clel 2431
  Copyright terms: Public domain W3C validator