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

Theorem syl5eqel 2369
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 12 . 2  |-  ( ph  ->  A  =  B )
3 syl5eqel.2 . 2  |-  ( ph  ->  B  e.  C )
42, 3eqeltrd 2359 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 6    = wceq 1624    e. wcel 1685
This theorem is referenced by:  syl5eqelr  2370  csbexg  3093  snex  4216  dmresexg  4978  f1oabexg  5450  cofunexg  5701  cofunex2g  5702  abrexex2g  5730  fovrn  5952  fnovrn  5957  xpexgALT  6032  fnwelem  6192  opiota  6284  riotaprop  6324  tfrlem12  6401  rdgseg  6431  oelim2  6589  oeeulem  6595  ecexg  6660  qsexg  6713  pmex  6773  resixpfo  6850  elixpsn  6851  unxpdomlem3  7065  fnfi  7130  rnfi  7137  iunfi  7140  unifi  7141  suppfif1  7145  pwfilem  7146  supexd  7200  oemapvali  7382  mapfien  7395  wemapwe  7396  cnfcomlem  7398  cnfcom  7399  cnfcom2lem  7400  cnfcom2  7401  cnfcom3lem  7402  cnfcom3  7403  prwf  7479  scott0  7552  htalem  7562  infxpenlem  7637  dfac8b  7654  cfss  7887  cofsmo  7891  coftr  7895  fin1a2lem10  8031  hsmexlem4  8051  hsmex2  8055  fpwwe  8264  canthwelem  8268  pwfseqlem1  8276  wuntp  8329  wunsn  8334  wunsuc  8335  wunr1om  8337  wunot  8341  r1limwun  8354  tsk1  8382  tsk2  8383  tskr1om  8385  gruuni  8418  grusn  8422  gruina  8436  wuncn  8788  negcl  9048  peano5nni  9745  peano5uzi  10096  quoremz  10954  quoremnn0ALT  10955  quoremnn0  10956  intfrac2  10957  intfracq  10958  seqf1olem1  11080  seqf1olem2  11081  serle  11096  discr1  11232  cats1cld  11500  sqrlem4  11726  sqreulem  11838  reccn2  12065  fsump1i  12227  fsumabs  12254  o1fsum  12266  supcvg  12309  mertenslem1  12335  mertenslem2  12336  rpnnen2  12499  ruclem12  12514  bitsfzolem  12620  bezoutlem2  12713  algrf  12738  algcvg  12741  algcvga  12744  algfx  12745  eucalgcvga  12751  eucalg  12752  prmdiv  12848  pythagtriplem11  12873  pythagtriplem13  12875  pcprecl  12887  infpnlem1  12952  infpnlem2  12953  4sqlem5  12984  mul4sqlem  12995  4sqlem13  12999  4sqlem14  13000  4sqlem17  13003  4sqlem18  13004  vdwlem5  13027  wunndx  13159  wunress  13202  restid  13333  mreexdomd  13546  acsfn0  13557  acsfn1  13558  acsfn2  13560  funcf2  13737  funcpropd  13769  fthepi  13797  ressffth  13807  elhomai2  13861  catcxpccl  13976  diag1cl  14011  yonedalem1  14041  spwex  14333  prdsinvlem  14598  subggrp  14619  nsgacs  14648  ghmima  14698  gimco  14727  gicref  14730  cayley  14784  cntrnsg  14812  oppgmnd  14822  efgredlemf  15045  efgredlemd  15048  efgredlemc  15049  cycsubgcyg  15182  gsumzaddlem  15198  gsum2d  15218  dprdfid  15247  dprd2dlem1  15271  dprd2da  15272  ablfacrplem  15295  ablfacrp  15296  ablfacrp2  15297  ablfac1lem  15298  pgpfac1lem1  15304  pgpfac1lem2  15305  pgpfac1lem3a  15306  pgpfac1lem3  15307  pgpfac1lem4  15308  pgpfac1lem5  15309  pgpfaclem1  15311  ablfaclem3  15317  opprrng  15408  subrgrng  15543  lmhmkerlss  15803  rlmlmod  15952  lidl0cl  15959  lidlacl  15960  lidlnegcl  15961  lidlmcl  15964  lidlacs  15968  fidomndrnglem  16042  gsumbagdiag  16117  psrass1lem  16118  mplsubrglem  16178  evlslem2  16244  vr1cl2  16267  vr1cl  16289  subrgvr1cl  16334  zlpirlem2  16437  zlpirlem3  16438  cygznlem1  16515  cygznlem2a  16516  cygznlem3  16518  isphld  16553  topopn  16647  rintopn  16650  fctop  16736  topcld  16767  intcld  16772  uncld  16773  unicld  16778  mretopd  16824  neiss2  16833  tgrest  16885  restin  16892  restcls  16906  restntr  16907  restlp  16908  restperf  16909  perfopn  16910  ordtbaslem  16913  ordtuni  16915  ordtbas2  16916  ordtbas  16917  ordttopon  16918  ordtopn1  16919  ordtopn2  16920  ordtrest2lem  16928  ordtrest2  16929  cnco  16990  cnrest  17008  cnprest2  17013  lmss  17021  cncmp  17114  imacmp  17119  fiuncmp  17126  concompcon  17153  cldllycmp  17216  hausmapdom  17221  kgentopon  17228  1stckgen  17244  ptbasin  17267  ptbasfi  17271  pttopon  17286  xkotopon  17290  txbasval  17296  ptpjcn  17300  ptcldmpt  17303  dfac14lem  17306  txcn  17315  ptcn  17316  ptrescn  17328  txkgen  17341  cnmpt12f  17355  xkofvcn  17373  qtopval2  17382  elqtop  17383  qtoptop2  17385  hmeoco  17458  idhmeo  17459  ordthmeolem  17487  ptunhmeo  17494  xkohmeo  17501  qtopf1  17502  cfinfil  17583  ufprim  17599  ufildr  17621  fin1aufil  17622  fmfg  17639  elfm3  17640  fbflim  17666  flimclslem  17674  flffbas  17685  cnpflf2  17690  flfcnp2  17697  fclsbas  17711  alexsublem  17733  ptcmplem3  17743  ptcmpg  17746  tgpsubcn  17768  tmdgsum  17773  symgtgp  17779  tmdlactcn  17780  submtmd  17782  clssubg  17786  divstgplem  17798  prdstmdd  17801  tsmsfbas  17805  eltsms  17810  tsmssubm  17820  dvrcn  17861  blres  17972  prdsbl  18032  metrest  18065  subgngp  18146  nlmvscnlem2  18191  nlmvscnlem1  18192  nrginvrcnlem  18196  qtopbaslem  18262  tgqioo  18301  icccmplem2  18323  icccmp  18325  reconnlem2  18327  xrge0tsms  18334  nmcn  18344  metnrmlem2  18359  divcn  18367  fsumcn  18369  fsum2cn  18370  cncfmet  18407  cdivcncf  18415  cnmpt2pc  18421  icchmeo  18434  cnrehmeo  18446  cnheiborlem  18447  bndth  18451  lebnumlem2  18455  htpycom  18469  htpyid  18470  htpyco1  18471  htpycc  18473  reparphti  18490  pcohtpylem  18512  pcoptcl  18514  pcoass  18517  pcorevcl  18518  pcorevlem  18519  ipcnlem2  18666  ipcnlem1  18667  cmsss  18767  minveclem4c  18784  minveclem3b  18787  minveclem4a  18789  minveclem4  18791  minveclem6  18793  pjthlem1  18796  ivthlem2  18807  ivthlem3  18808  ovolicc2lem4  18874  finiunmbl  18896  voliunlem1  18902  ioombl1lem1  18910  ioombl1lem3  18912  ioombl1lem4  18913  ovolioo  18920  opnmblALT  18953  mbfimaicc  18983  mbfid  18986  mbfeqalem  18992  mbfres  18994  cncombf  19008  itg1addlem4  19049  mbfi1flim  19073  itg2monolem2  19101  itg2monolem3  19102  itg2mono  19103  itg2cnlem1  19111  itgcl  19133  iblss  19154  itgeqa  19163  itgss3  19164  itgless  19166  iblconst  19167  ibladdlem  19169  itgaddlem1  19172  iblabslem  19177  iblabsr  19179  iblmulc2  19180  itggt0  19191  itgcn  19192  limcvallem  19216  limcflflem  19225  limcres  19231  cnplimc  19232  limccnp  19236  limccnp2  19237  dvreslem  19254  dvres2lem  19255  dvcnp  19263  dvnff  19267  dvmptres2  19306  dvmptres  19307  dvmptntr  19315  dvmptfsum  19317  dvcnvlem  19318  dvcnv  19319  dvferm1lem  19326  dvferm2lem  19328  dvlipcn  19336  dvlip2  19337  c1liplem1  19338  lhop1lem  19355  dvcnvrelem2  19360  dvcvx  19362  dvfsumge  19364  dvfsumlem3  19370  ftc1lem3  19380  ftc1lem4  19381  evl1rhm  19407  ply1remlem  19543  ply0  19585  plyid  19586  plyeq0lem  19587  dgrub  19611  dgrub2  19612  dgrlb  19613  coeidlem  19614  coeaddlem  19625  coemullem  19626  coemulhi  19630  dgreq0  19641  dgrlt  19642  dgradd2  19644  dgrmul  19646  dgrcolem2  19650  dgrco  19651  plycj  19653  coecj  19654  plydivlem2  19669  plydivlem4  19671  plyremlem  19679  plyrem  19680  quotcan  19684  vieta1lem1  19685  elqaalem2  19695  elqaalem3  19696  radcnvcl  19788  psercnlem1  19796  pserdvlem2  19799  pilem2  19823  pilem3  19824  logfac  19949  logcnlem2  19985  logcnlem3  19986  logcnlem4  19987  dvlog  19993  cxpcn  20080  cxpcn3lem  20082  ang180lem1  20102  ang180lem2  20103  ang180lem3  20104  pythag  20110  quart1lem  20146  xrlimcnp  20258  efrlim  20259  ftalem1  20305  ftalem2  20306  ftalem4  20308  ftalem5  20309  basellem1  20313  basellem2  20314  basellem3  20315  basellem4  20316  basellem5  20317  basellem8  20320  dchr1cl  20485  dchrinvcl  20487  dchrptlem1  20498  dchrptlem2  20499  bposlem3  20520  bposlem5  20522  bposlem6  20523  lgsqrlem2  20576  lgsqrlem3  20577  lgsqrlem4  20578  lgseisenlem1  20583  lgseisenlem2  20584  lgseisenlem3  20585  lgseisenlem4  20586  lgsquadlem1  20588  lgsquadlem2  20589  lgsquadlem3  20590  2sqlem8  20606  chebbnd1lem1  20613  chebbnd1lem2  20614  chebbnd1lem3  20615  mulog2sumlem2  20679  selberglem2  20690  chpdifbndlem1  20697  chpdifbndlem2  20698  pntrmax  20708  pntpbnd1a  20729  pntpbnd1  20730  pntpbnd2  20731  pntibndlem1  20733  pntibndlem2  20735  pntibndlem3  20736  pntlemd  20738  pntlemc  20739  pntlema  20740  pntlemg  20742  pntlemr  20746  pntlemj  20747  ostth2lem2  20778  ostth2lem3  20779  ostth2lem4  20780  ostth2  20781  ostth3  20782  grpoinvfval  20884  grpodivfval  20902  gxfval  20917  ghgrp  21028  isvc  21130  isnv  21161  imsmet  21253  smcnlem  21263  minvecolem2  21447  minvecolem3  21448  minvecolem4c  21451  minvecolem4  21452  minvecolem5  21453  minvecolem6  21454  hhssabloi  21832  pjhthlem1  21963  pjoc1i  22003  cnlnadjlem3  22642  cnlnadjlem5  22644  mdsymlem1  22976  mdsymlem3  22978  dmgmseqn0  23101  erdsze2lem1  23139  erdsze2lem2  23140  txsconlem  23176  cvxpcon  23178  cvxscon  23179  cvmsiota  23213  cvmliftiota  23237  cvmlift2lem10  23248  ghomgrp  23402  axfelem2  23749  altxpsspw  23919  eleesub  23947  axsegconlem2  23954  axsegconlem8  23960  axlowdimlem7  23984  axlowdimlem17  23994  hfuni  24222  inpws2  24442  fnovrn2  24449  fldrels  24512  isprj2  24564  iscst1  24574  valcurfn1  24604  ppldrels  24627  supdef  24662  supdefa  24663  defge3  24671  inposet  24678  tolat  24686  toplat  24690  unsgrp  24767  trset  24792  ltrset  24802  rltrset  24813  inttop3  24916  qusp  24942  istopxc  24948  limvinlv  24959  conttnf2  24962  exopcopn  24972  prdnei  24973  limptlimpr2lem1  24974  limptlimpr2lem2  24975  islimrs3  24981  islimrs4  24982  bwt2  24992  flfneicn  25025  supbrr  25036  carinttar  25302  prismorcsetlemb  25313  cmpidmor2  25369  isconc1  25406  pgapspf  25452  iscola2  25492  locfindis  25705  tailf  25724  tailfb  25726  supex2g  25819  sdclem1  25853  constcncf  25878  addccncf  25879  sub1cncf  25881  sub2cncf  25882  sstotbnd2  25898  equivbnd2  25916  ismtyres  25932  rrnheibor  25961  reheibor  25963  iccbnd  25964  icccmpALT  25965  exidres  25968  exidresid  25969  mzpnegmpt  26222  vdioph  26259  3anrabdioph  26262  3orrabdioph  26263  rexrabdioph  26275  rexfrabdioph  26276  2rexfrabdioph  26277  3rexfrabdioph  26278  4rexfrabdioph  26279  6rexfrabdioph  26280  7rexfrabdioph  26281  elnnrabdioph  26288  dvdsrabdioph  26291  eldioph4b  26294  pellfundgt1  26368  jm2.27c  26500  lsmfgcl  26572  lmhmfgima  26582  lmhmlnmsplit  26585  pwssplit4  26591  pwslnm  26596  uvcff  26640  frlmsplit2  26643  lindsmm  26698  psgndmsubg  26825  sblpnf  26939  fsumcnf  27092  refsum2cnlem1  27108  fmulcl  27111  itgsinexplem1  27148  stoweidlem2  27151  stoweidlem3  27152  stoweidlem5  27154  stoweidlem20  27169  stoweidlem21  27170  stoweidlem22  27171  stoweidlem23  27172  stoweidlem31  27180  stoweidlem32  27181  stoweidlem35  27184  stoweidlem36  27185  stoweidlem40  27189  stoweidlem41  27190  stoweidlem47  27196  stoweidlem50  27199  stoweidlem57  27206  stoweidlem59  27208  stoweidlem60  27209  stoweidlem62  27211  wallispi2lem2  27221  dp2cl  27500  bnj893  28228  bnj944  28238  bnj969  28246  bnj1136  28295  bnj1177  28304  bnj1452  28350  bnj1489  28354  lshpinN  28447  dalemdea  29119  dalem5  29124  dalem8  29127  dalem9  29129  dalem15  29135  dalem23  29153  cdlemblem  29250  osumcllem1N  29413  osumcllem9N  29421  pexmidlem6N  29432  lhpat2  29502  arglem1N  29647  cdleme0aa  29667  cdleme1b  29683  cdleme1  29684  cdleme2  29685  cdleme3b  29686  cdleme3e  29689  cdleme3h  29692  cdleme7b  29701  cdleme7e  29704  cdleme7ga  29705  cdleme9b  29709  cdleme15d  29734  cdleme22gb  29751  cdlemedb  29754  cdlemeda  29755  cdleme23b  29807  cdleme25cl  29814  cdleme27cl  29823  cdleme29cl  29834  cdlemefs27cl  29870  cdleme42c  29929  cdleme42h  29939  cdleme42i  29940  cdlemg4c  30069  cdlemg4  30074  cdlemg6c  30077  cdlemkvcl  30299  cdlemkoatnle  30308  cdlemk14  30311  cdlemk15  30312  cdlemk29-3  30368  cdlemk37  30371  dia2dimlem1  30522  dvheveccl  30570  diblss  30628  dihglblem5  30756  dih1dimatlem  30787  dihat  30793  dihjatcclem1  30876  dihjatcclem2  30877  dihjatcclem4  30879  dochexmidlem5  30922  dochexmidlem6  30923  lclkrlem2m  30977  lclkrlem2o  30979  lcfrlem3  31002  lcfrlem22  31022  lcfrlem25  31025  lcfrlem30  31030  lcfrlem37  31037  mapdpglem17N  31146  mapdpglem19  31148  hdmap1val  31257
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-11 1716  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1530  df-cleq 2278  df-clel 2281
  Copyright terms: Public domain W3C validator