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

Theorem syl5eqel 2520
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 2510 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  2521  csbexg  3261  snex  4405  dmresexg  5169  f1oabexg  5686  cofunexg  5959  cofunex2g  5960  abrexex2g  5988  fovrn  6216  fnovrn  6221  xpexgALT  6297  fnwelem  6461  opiota  6535  riotaprop  6573  tfrlem12  6650  rdgseg  6680  oelim2  6838  oeeulem  6844  ecexg  6909  qsexg  6962  pmex  7023  resixpfo  7100  elixpsn  7101  unxpdomlem3  7315  rabfi  7333  fnfi  7384  rnfi  7391  iunfi  7394  unifi  7395  suppfif1  7400  pwfilem  7401  supexd  7458  oemapvali  7640  mapfien  7653  wemapwe  7654  cnfcomlem  7656  cnfcom  7657  cnfcom2lem  7658  cnfcom2  7659  cnfcom3lem  7660  cnfcom3  7661  prwf  7737  scott0  7810  htalem  7820  infxpenlem  7895  dfac8b  7912  cfss  8145  cofsmo  8149  coftr  8153  fin1a2lem10  8289  hsmexlem4  8309  hsmex2  8313  fpwwe  8521  canthwelem  8525  pwfseqlem1  8533  wuntp  8586  wunsn  8591  wunsuc  8592  wunr1om  8594  wunot  8598  r1limwun  8611  tsk1  8639  tsk2  8640  tskr1om  8642  gruuni  8675  grusn  8679  gruina  8693  wuncn  9045  negcl  9306  peano5nni  10003  peano5uzi  10358  quoremz  11236  quoremnn0  11237  quoremnn0ALT  11238  intfrac2  11239  intfracq  11240  seqf1olem1  11362  seqf1olem2  11363  serle  11378  discr1  11515  cats1cld  11819  sqrlem4  12051  sqreulem  12163  reccn2  12390  fsump1i  12553  fsumabs  12580  o1fsum  12592  supcvg  12635  mertenslem1  12661  mertenslem2  12662  rpnnen2  12825  ruclem12  12840  bitsfzolem  12946  bezoutlem2  13039  algrf  13064  algcvg  13067  algcvga  13070  algfx  13071  eucalgcvga  13077  eucalg  13078  prmdiv  13174  pythagtriplem11  13199  pythagtriplem13  13201  pcprecl  13213  infpnlem1  13278  infpnlem2  13279  4sqlem5  13310  mul4sqlem  13321  4sqlem13  13325  4sqlem14  13326  4sqlem17  13329  4sqlem18  13330  vdwlem5  13353  wunndx  13485  wunress  13528  restid  13661  mreexdomd  13874  acsfn0  13885  acsfn1  13886  acsfn2  13888  funcf2  14065  funcpropd  14097  fthepi  14125  ressffth  14135  elhomai2  14189  catcxpccl  14304  diag1cl  14339  yonedalem1  14369  spwex  14661  prdsinvlem  14926  subggrp  14947  nsgacs  14976  ghmima  15026  gimco  15055  gicref  15058  cayley  15112  cntrnsg  15140  oppgmnd  15150  efgredlemf  15373  efgredlemd  15376  efgredlemc  15377  cycsubgcyg  15510  gsumzaddlem  15526  gsum2d  15546  dprdfid  15575  dprd2dlem1  15599  dprd2da  15600  ablfacrplem  15623  ablfacrp  15624  ablfacrp2  15625  ablfac1lem  15626  pgpfac1lem1  15632  pgpfac1lem2  15633  pgpfac1lem3a  15634  pgpfac1lem3  15635  pgpfac1lem4  15636  pgpfac1lem5  15637  pgpfaclem1  15639  ablfaclem3  15645  opprrng  15736  subrgrng  15871  lmhmkerlss  16127  rlmlmod  16276  lidl0cl  16283  lidlacl  16284  lidlnegcl  16285  lidlmcl  16288  lidlacs  16292  fidomndrnglem  16366  gsumbagdiag  16441  psrass1lem  16442  mplsubrglem  16502  evlslem2  16568  vr1cl2  16591  vr1cl  16611  subrgvr1cl  16655  zlpirlem2  16769  zlpirlem3  16770  cygznlem1  16847  cygznlem2a  16848  cygznlem3  16850  isphld  16885  topopn  16979  rintopn  16982  fctop  17068  topcld  17099  intcld  17104  uncld  17105  unicld  17110  mretopd  17156  neiptoptop  17195  tgrest  17223  restin  17230  neitr  17244  restcls  17245  restntr  17246  restlp  17247  restperf  17248  perfopn  17249  ordtbaslem  17252  ordtuni  17254  ordtbas2  17255  ordtbas  17256  ordttopon  17257  ordtopn1  17258  ordtopn2  17259  ordtrest2lem  17267  ordtrest2  17268  cnco  17330  cnrest  17349  cnprest2  17354  lmss  17362  cncmp  17455  imacmp  17460  fiuncmp  17467  bwth  17473  concompcon  17495  cldllycmp  17558  hausmapdom  17563  kgentopon  17570  1stckgen  17586  ptbasin  17609  ptbasfi  17613  pttopon  17628  xkotopon  17632  txbasval  17638  ptpjcn  17643  ptcldmpt  17646  dfac14lem  17649  txcn  17658  ptcn  17659  ptrescn  17671  txkgen  17684  cnmpt12f  17698  xkofvcn  17716  qtopval2  17728  elqtop  17729  qtoptop2  17731  hmeoco  17804  idhmeo  17805  ordthmeolem  17833  ptunhmeo  17840  xkohmeo  17847  qtopf1  17848  cfinfil  17925  ufprim  17941  ufildr  17963  fin1aufil  17964  fmfg  17981  elfm3  17982  fbflim  18008  flimclslem  18016  flffbas  18027  cnpflf2  18032  flfcnp2  18039  fclsbas  18053  alexsublem  18075  ptcmplem3  18085  ptcmpg  18088  cnextcn  18098  tgpsubcn  18120  tmdgsum  18125  symgtgp  18131  tmdlactcn  18132  submtmd  18134  clssubg  18138  divstgplem  18150  prdstmdd  18153  tsmsfbas  18157  eltsms  18162  tsmssubm  18172  dvrcn  18213  utop2nei  18280  utop3cls  18281  utopreg  18282  blres  18461  prdsbl  18521  metrest  18554  metustexhalfOLD  18593  metustexhalf  18594  subgngp  18676  nlmvscnlem2  18721  nlmvscnlem1  18722  nrginvrcnlem  18726  qtopbaslem  18792  tgqioo  18831  icccmplem2  18854  icccmp  18856  reconnlem2  18858  xrge0tsms  18865  nmcn  18875  metnrmlem2  18890  divcn  18898  fsumcn  18900  fsum2cn  18901  cncfmet  18938  addccncf  18946  cnmpt2pc  18953  icchmeo  18966  cnrehmeo  18978  cnheiborlem  18979  bndth  18983  lebnumlem2  18987  htpycom  19001  htpyid  19002  htpyco1  19003  htpycc  19005  reparphti  19022  pcohtpylem  19044  pcoptcl  19046  pcoass  19049  pcorevcl  19050  pcorevlem  19051  ipcnlem2  19198  ipcnlem1  19199  cmsss  19303  minveclem4c  19326  minveclem3b  19329  minveclem4a  19331  minveclem4  19333  minveclem6  19335  pjthlem1  19338  ivthlem2  19349  ivthlem3  19350  ovolicc2lem4  19416  finiunmbl  19438  voliunlem1  19444  ioombl1lem1  19452  ioombl1lem3  19454  ioombl1lem4  19455  ovolioo  19462  opnmblALT  19495  mbfimaicc  19525  mbfid  19528  mbfeqalem  19534  mbfres  19536  cncombf  19550  mbfi1flim  19615  itg2monolem2  19643  itg2monolem3  19644  itg2mono  19645  itg2cnlem1  19653  itgcl  19675  iblss  19696  itgeqa  19705  itgss3  19706  itgless  19708  iblconst  19709  ibladdlem  19711  itgaddlem1  19714  iblabslem  19719  iblabsr  19721  iblmulc2  19722  itggt0  19733  itgcn  19734  limcvallem  19758  limcflflem  19767  limcres  19773  cnplimc  19774  limccnp  19778  limccnp2  19779  dvreslem  19796  dvres2lem  19797  dvcnp  19805  dvnff  19809  dvmptres2  19848  dvmptres  19849  dvmptntr  19857  dvmptfsum  19859  dvcnvlem  19860  dvcnv  19861  dvferm1lem  19868  dvferm2lem  19870  dvlipcn  19878  dvlip2  19879  c1liplem1  19880  lhop1lem  19897  dvcnvrelem2  19902  dvcvx  19904  dvfsumge  19906  dvfsumlem3  19912  ftc1lem3  19922  ftc1lem4  19923  evl1rhm  19949  ply1remlem  20085  ply0  20127  plyid  20128  plyeq0lem  20129  dgrub  20153  dgrub2  20154  dgrlb  20155  coeidlem  20156  coeaddlem  20167  coemullem  20168  coemulhi  20172  dgreq0  20183  dgrlt  20184  dgradd2  20186  dgrmul  20188  dgrcolem2  20192  dgrco  20193  plycj  20195  coecj  20196  plydivlem2  20211  plydivlem4  20213  plyremlem  20221  plyrem  20222  quotcan  20226  vieta1lem1  20227  elqaalem2  20237  elqaalem3  20238  radcnvcl  20333  psercnlem1  20341  pserdvlem2  20344  pilem2  20368  pilem3  20369  logfac  20495  logcnlem2  20534  logcnlem3  20535  logcnlem4  20536  dvlog  20542  cxpcn  20629  cxpcn3lem  20631  ang180lem1  20651  ang180lem2  20652  ang180lem3  20653  pythag  20659  quart1lem  20695  xrlimcnp  20807  efrlim  20808  ftalem1  20855  ftalem2  20856  ftalem4  20858  ftalem5  20859  basellem1  20863  basellem2  20864  basellem3  20865  basellem4  20866  basellem5  20867  basellem8  20870  dchr1cl  21035  dchrinvcl  21037  dchrptlem1  21048  dchrptlem2  21049  bposlem3  21070  bposlem5  21072  bposlem6  21073  lgsqrlem2  21126  lgsqrlem3  21127  lgsqrlem4  21128  lgseisenlem1  21133  lgseisenlem2  21134  lgseisenlem3  21135  lgseisenlem4  21136  lgsquadlem1  21138  lgsquadlem2  21139  lgsquadlem3  21140  2sqlem8  21156  chebbnd1lem1  21163  chebbnd1lem2  21164  chebbnd1lem3  21165  mulog2sumlem2  21229  selberglem2  21240  chpdifbndlem1  21247  chpdifbndlem2  21248  pntrmax  21258  pntpbnd1a  21279  pntpbnd1  21280  pntpbnd2  21281  pntibndlem1  21283  pntibndlem2  21285  pntibndlem3  21286  pntlemd  21288  pntlemc  21289  pntlema  21290  pntlemg  21292  pntlemr  21296  pntlemj  21297  ostth2lem2  21328  ostth2lem3  21329  ostth2lem4  21330  ostth2  21331  ostth3  21332  usgrares1  21424  usgrafilem2  21426  cusgraexilem1  21475  cusgrares  21481  cusgrasizeinds  21485  cusgrafilem3  21490  wlks  21526  trls  21536  grpoinvfval  21812  grpodivfval  21830  gxfval  21845  ghgrp  21956  isvc  22060  isnv  22091  imsmet  22183  smcnlem  22193  minvecolem2  22377  minvecolem3  22378  minvecolem4c  22381  minvecolem4  22382  minvecolem5  22383  minvecolem6  22384  hhssabloi  22762  pjhthlem1  22893  pjoc1i  22933  cnlnadjlem3  23572  cnlnadjlem5  23574  mdsymlem1  23906  mdsymlem3  23908  abrexexd  23990  elovimad  24051  xrge0pluscn  24326  prsiga  24514  inelsiga  24518  mbfmcst  24609  mbfmco  24614  mbfmcnt  24618  dya2icoseg  24627  sibf0  24649  sibff  24651  sibfof  24654  sitgclg  24656  0rrv  24709  rrvsum  24712  erdsze2lem1  24889  erdsze2lem2  24890  txsconlem  24927  cvxpcon  24929  cvxscon  24930  cvmsiota  24964  cvmliftiota  24988  cvmlift2lem10  24999  ghomgrp  25101  wsucex  25577  wsuccl  25578  nobndlem2  25648  nofulllem4  25660  altxpsspw  25822  eleesub  25850  axsegconlem2  25857  axsegconlem8  25863  axlowdimlem7  25887  axlowdimlem17  25897  hfuni  26125  mbfresfi  26253  mbfposadd  26254  cnambfre  26255  itg2addnclem2  26257  ibladdnclem  26261  itgaddnclem1  26263  iblabsnclem  26268  iblmulc2nc  26270  itggt0cn  26277  ftc1cnnclem  26278  ftc1anclem3  26282  ftc1anclem5  26284  ftc1anclem8  26287  ftc1anc  26288  locfindis  26385  tailf  26404  tailfb  26406  supex2g  26439  sdclem1  26447  constcncf  26468  sub1cncf  26470  sub2cncf  26471  sstotbnd2  26483  equivbnd2  26501  ismtyres  26517  rrnheibor  26546  reheibor  26548  iccbnd  26549  icccmpALT  26550  exidres  26553  exidresid  26554  mzpnegmpt  26801  vdioph  26838  3anrabdioph  26841  3orrabdioph  26842  rexrabdioph  26854  rexfrabdioph  26855  2rexfrabdioph  26856  3rexfrabdioph  26857  4rexfrabdioph  26858  6rexfrabdioph  26859  7rexfrabdioph  26860  elnnrabdioph  26867  dvdsrabdioph  26870  eldioph4b  26872  pellfundgt1  26946  jm2.27c  27078  lsmfgcl  27149  lmhmfgima  27159  lmhmlnmsplit  27162  pwssplit4  27168  pwslnm  27173  uvcff  27217  frlmsplit2  27220  lindsmm  27275  psgndmsubg  27402  sblpnf  27516  fsumcnf  27668  refsum2cnlem1  27684  fmulcl  27687  itgsin0pilem1  27720  itgsinexplem1  27724  stoweidlem2  27727  stoweidlem3  27728  stoweidlem5  27730  stoweidlem16  27741  stoweidlem18  27743  stoweidlem20  27745  stoweidlem21  27746  stoweidlem22  27747  stoweidlem23  27748  stoweidlem31  27756  stoweidlem32  27757  stoweidlem35  27760  stoweidlem36  27761  stoweidlem40  27765  stoweidlem41  27766  stoweidlem47  27772  stoweidlem50  27775  stoweidlem57  27782  stoweidlem59  27784  stoweidlem60  27785  stoweidlem62  27787  wallispi2lem2  27797  el2xptp0  28061  otel3xp  28062  swrdccatin2  28210  swrdccatin12lem3  28212  swrdccatin12  28214  swrdccat3  28215  swrdccat3a  28217  frgrawopreglem1  28433  dp2cl  28512  bnj893  29299  bnj944  29309  bnj969  29317  bnj1136  29366  bnj1177  29375  bnj1452  29421  bnj1489  29425  lshpinN  29787  dalemdea  30459  dalem5  30464  dalem8  30467  dalem9  30469  dalem15  30475  dalem23  30493  cdlemblem  30590  osumcllem1N  30753  osumcllem9N  30761  pexmidlem6N  30772  lhpat2  30842  arglem1N  30987  cdleme0aa  31007  cdleme1b  31023  cdleme1  31024  cdleme2  31025  cdleme3b  31026  cdleme3e  31029  cdleme3h  31032  cdleme7b  31041  cdleme7e  31044  cdleme7ga  31045  cdleme9b  31049  cdleme15d  31074  cdleme22gb  31091  cdlemedb  31094  cdlemeda  31095  cdleme23b  31147  cdleme25cl  31154  cdleme27cl  31163  cdleme29cl  31174  cdlemefs27cl  31210  cdleme42c  31269  cdleme42h  31279  cdleme42i  31280  cdlemg4c  31409  cdlemg4  31414  cdlemg6c  31417  cdlemkvcl  31639  cdlemkoatnle  31648  cdlemk14  31651  cdlemk15  31652  cdlemk29-3  31708  cdlemk37  31711  dia2dimlem1  31862  dvheveccl  31910  diblss  31968  dihglblem5  32096  dih1dimatlem  32127  dihat  32133  dihjatcclem1  32216  dihjatcclem2  32217  dihjatcclem4  32219  dochexmidlem5  32262  dochexmidlem6  32263  lclkrlem2m  32317  lclkrlem2o  32319  lcfrlem3  32342  lcfrlem22  32362  lcfrlem25  32365  lcfrlem30  32370  lcfrlem37  32377  mapdpglem17N  32486  mapdpglem19  32488  hdmap1val  32597
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 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-cleq 2429  df-clel 2432
  Copyright terms: Public domain W3C validator