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

Theorem syl5eqel 2367
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 10 . 2  |-  ( ph  ->  A  =  B )
3 syl5eqel.2 . 2  |-  ( ph  ->  B  e.  C )
42, 3eqeltrd 2357 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684
This theorem is referenced by:  syl5eqelr  2368  csbexg  3091  snex  4216  dmresexg  4978  f1oabexg  5484  cofunexg  5739  cofunex2g  5740  abrexex2g  5768  fovrn  5990  fnovrn  5995  xpexgALT  6070  fnwelem  6230  opiota  6290  riotaprop  6328  tfrlem12  6405  rdgseg  6435  oelim2  6593  oeeulem  6599  ecexg  6664  qsexg  6717  pmex  6777  resixpfo  6854  elixpsn  6855  unxpdomlem3  7069  fnfi  7134  rnfi  7141  iunfi  7144  unifi  7145  suppfif1  7149  pwfilem  7150  supexd  7204  oemapvali  7386  mapfien  7399  wemapwe  7400  cnfcomlem  7402  cnfcom  7403  cnfcom2lem  7404  cnfcom2  7405  cnfcom3lem  7406  cnfcom3  7407  prwf  7483  scott0  7556  htalem  7566  infxpenlem  7641  dfac8b  7658  cfss  7891  cofsmo  7895  coftr  7899  fin1a2lem10  8035  hsmexlem4  8055  hsmex2  8059  fpwwe  8268  canthwelem  8272  pwfseqlem1  8280  wuntp  8333  wunsn  8338  wunsuc  8339  wunr1om  8341  wunot  8345  r1limwun  8358  tsk1  8386  tsk2  8387  tskr1om  8389  gruuni  8422  grusn  8426  gruina  8440  wuncn  8792  negcl  9052  peano5nni  9749  peano5uzi  10100  quoremz  10959  quoremnn0  10960  quoremnn0ALT  10961  intfrac2  10962  intfracq  10963  seqf1olem1  11085  seqf1olem2  11086  serle  11101  discr1  11237  cats1cld  11505  sqrlem4  11731  sqreulem  11843  reccn2  12070  fsump1i  12232  fsumabs  12259  o1fsum  12271  supcvg  12314  mertenslem1  12340  mertenslem2  12341  rpnnen2  12504  ruclem12  12519  bitsfzolem  12625  bezoutlem2  12718  algrf  12743  algcvg  12746  algcvga  12749  algfx  12750  eucalgcvga  12756  eucalg  12757  prmdiv  12853  pythagtriplem11  12878  pythagtriplem13  12880  pcprecl  12892  infpnlem1  12957  infpnlem2  12958  4sqlem5  12989  mul4sqlem  13000  4sqlem13  13004  4sqlem14  13005  4sqlem17  13008  4sqlem18  13009  vdwlem5  13032  wunndx  13164  wunress  13207  restid  13338  mreexdomd  13551  acsfn0  13562  acsfn1  13563  acsfn2  13565  funcf2  13742  funcpropd  13774  fthepi  13802  ressffth  13812  elhomai2  13866  catcxpccl  13981  diag1cl  14016  yonedalem1  14046  spwex  14338  prdsinvlem  14603  subggrp  14624  nsgacs  14653  ghmima  14703  gimco  14732  gicref  14735  cayley  14789  cntrnsg  14817  oppgmnd  14827  efgredlemf  15050  efgredlemd  15053  efgredlemc  15054  cycsubgcyg  15187  gsumzaddlem  15203  gsum2d  15223  dprdfid  15252  dprd2dlem1  15276  dprd2da  15277  ablfacrplem  15300  ablfacrp  15301  ablfacrp2  15302  ablfac1lem  15303  pgpfac1lem1  15309  pgpfac1lem2  15310  pgpfac1lem3a  15311  pgpfac1lem3  15312  pgpfac1lem4  15313  pgpfac1lem5  15314  pgpfaclem1  15316  ablfaclem3  15322  opprrng  15413  subrgrng  15548  lmhmkerlss  15808  rlmlmod  15957  lidl0cl  15964  lidlacl  15965  lidlnegcl  15966  lidlmcl  15969  lidlacs  15973  fidomndrnglem  16047  gsumbagdiag  16122  psrass1lem  16123  mplsubrglem  16183  evlslem2  16249  vr1cl2  16272  vr1cl  16294  subrgvr1cl  16339  zlpirlem2  16442  zlpirlem3  16443  cygznlem1  16520  cygznlem2a  16521  cygznlem3  16523  isphld  16558  topopn  16652  rintopn  16655  fctop  16741  topcld  16772  intcld  16777  uncld  16778  unicld  16783  mretopd  16829  neiss2  16838  tgrest  16890  restin  16897  restcls  16911  restntr  16912  restlp  16913  restperf  16914  perfopn  16915  ordtbaslem  16918  ordtuni  16920  ordtbas2  16921  ordtbas  16922  ordttopon  16923  ordtopn1  16924  ordtopn2  16925  ordtrest2lem  16933  ordtrest2  16934  cnco  16995  cnrest  17013  cnprest2  17018  lmss  17026  cncmp  17119  imacmp  17124  fiuncmp  17131  concompcon  17158  cldllycmp  17221  hausmapdom  17226  kgentopon  17233  1stckgen  17249  ptbasin  17272  ptbasfi  17276  pttopon  17291  xkotopon  17295  txbasval  17301  ptpjcn  17305  ptcldmpt  17308  dfac14lem  17311  txcn  17320  ptcn  17321  ptrescn  17333  txkgen  17346  cnmpt12f  17360  xkofvcn  17378  qtopval2  17387  elqtop  17388  qtoptop2  17390  hmeoco  17463  idhmeo  17464  ordthmeolem  17492  ptunhmeo  17499  xkohmeo  17506  qtopf1  17507  cfinfil  17588  ufprim  17604  ufildr  17626  fin1aufil  17627  fmfg  17644  elfm3  17645  fbflim  17671  flimclslem  17679  flffbas  17690  cnpflf2  17695  flfcnp2  17702  fclsbas  17716  alexsublem  17738  ptcmplem3  17748  ptcmpg  17751  tgpsubcn  17773  tmdgsum  17778  symgtgp  17784  tmdlactcn  17785  submtmd  17787  clssubg  17791  divstgplem  17803  prdstmdd  17806  tsmsfbas  17810  eltsms  17815  tsmssubm  17825  dvrcn  17866  blres  17977  prdsbl  18037  metrest  18070  subgngp  18151  nlmvscnlem2  18196  nlmvscnlem1  18197  nrginvrcnlem  18201  qtopbaslem  18267  tgqioo  18306  icccmplem2  18328  icccmp  18330  reconnlem2  18332  xrge0tsms  18339  nmcn  18349  metnrmlem2  18364  divcn  18372  fsumcn  18374  fsum2cn  18375  cncfmet  18412  cdivcncf  18420  cnmpt2pc  18426  icchmeo  18439  cnrehmeo  18451  cnheiborlem  18452  bndth  18456  lebnumlem2  18460  htpycom  18474  htpyid  18475  htpyco1  18476  htpycc  18478  reparphti  18495  pcohtpylem  18517  pcoptcl  18519  pcoass  18522  pcorevcl  18523  pcorevlem  18524  ipcnlem2  18671  ipcnlem1  18672  cmsss  18772  minveclem4c  18789  minveclem3b  18792  minveclem4a  18794  minveclem4  18796  minveclem6  18798  pjthlem1  18801  ivthlem2  18812  ivthlem3  18813  ovolicc2lem4  18879  finiunmbl  18901  voliunlem1  18907  ioombl1lem1  18915  ioombl1lem3  18917  ioombl1lem4  18918  ovolioo  18925  opnmblALT  18958  mbfimaicc  18988  mbfid  18991  mbfeqalem  18997  mbfres  18999  cncombf  19013  itg1addlem4  19054  mbfi1flim  19078  itg2monolem2  19106  itg2monolem3  19107  itg2mono  19108  itg2cnlem1  19116  itgcl  19138  iblss  19159  itgeqa  19168  itgss3  19169  itgless  19171  iblconst  19172  ibladdlem  19174  itgaddlem1  19177  iblabslem  19182  iblabsr  19184  iblmulc2  19185  itggt0  19196  itgcn  19197  limcvallem  19221  limcflflem  19230  limcres  19236  cnplimc  19237  limccnp  19241  limccnp2  19242  dvreslem  19259  dvres2lem  19260  dvcnp  19268  dvnff  19272  dvmptres2  19311  dvmptres  19312  dvmptntr  19320  dvmptfsum  19322  dvcnvlem  19323  dvcnv  19324  dvferm1lem  19331  dvferm2lem  19333  dvlipcn  19341  dvlip2  19342  c1liplem1  19343  lhop1lem  19360  dvcnvrelem2  19365  dvcvx  19367  dvfsumge  19369  dvfsumlem3  19375  ftc1lem3  19385  ftc1lem4  19386  evl1rhm  19412  ply1remlem  19548  ply0  19590  plyid  19591  plyeq0lem  19592  dgrub  19616  dgrub2  19617  dgrlb  19618  coeidlem  19619  coeaddlem  19630  coemullem  19631  coemulhi  19635  dgreq0  19646  dgrlt  19647  dgradd2  19649  dgrmul  19651  dgrcolem2  19655  dgrco  19656  plycj  19658  coecj  19659  plydivlem2  19674  plydivlem4  19676  plyremlem  19684  plyrem  19685  quotcan  19689  vieta1lem1  19690  elqaalem2  19700  elqaalem3  19701  radcnvcl  19793  psercnlem1  19801  pserdvlem2  19804  pilem2  19828  pilem3  19829  logfac  19954  logcnlem2  19990  logcnlem3  19991  logcnlem4  19992  dvlog  19998  cxpcn  20085  cxpcn3lem  20087  ang180lem1  20107  ang180lem2  20108  ang180lem3  20109  pythag  20115  quart1lem  20151  xrlimcnp  20263  efrlim  20264  ftalem1  20310  ftalem2  20311  ftalem4  20313  ftalem5  20314  basellem1  20318  basellem2  20319  basellem3  20320  basellem4  20321  basellem5  20322  basellem8  20325  dchr1cl  20490  dchrinvcl  20492  dchrptlem1  20503  dchrptlem2  20504  bposlem3  20525  bposlem5  20527  bposlem6  20528  lgsqrlem2  20581  lgsqrlem3  20582  lgsqrlem4  20583  lgseisenlem1  20588  lgseisenlem2  20589  lgseisenlem3  20590  lgseisenlem4  20591  lgsquadlem1  20593  lgsquadlem2  20594  lgsquadlem3  20595  2sqlem8  20611  chebbnd1lem1  20618  chebbnd1lem2  20619  chebbnd1lem3  20620  mulog2sumlem2  20684  selberglem2  20695  chpdifbndlem1  20702  chpdifbndlem2  20703  pntrmax  20713  pntpbnd1a  20734  pntpbnd1  20735  pntpbnd2  20736  pntibndlem1  20738  pntibndlem2  20740  pntibndlem3  20741  pntlemd  20743  pntlemc  20744  pntlema  20745  pntlemg  20747  pntlemr  20751  pntlemj  20752  ostth2lem2  20783  ostth2lem3  20784  ostth2lem4  20785  ostth2  20786  ostth3  20787  grpoinvfval  20891  grpodivfval  20909  gxfval  20924  ghgrp  21035  isvc  21137  isnv  21168  imsmet  21260  smcnlem  21270  minvecolem2  21454  minvecolem3  21455  minvecolem4c  21458  minvecolem4  21459  minvecolem5  21460  minvecolem6  21461  hhssabloi  21839  pjhthlem1  21970  pjoc1i  22010  cnlnadjlem3  22649  cnlnadjlem5  22651  mdsymlem1  22983  mdsymlem3  22985  rabfi  23170  abrexexd  23192  xrge0pluscn  23322  mbfmcst  23564  mbfmco  23569  dya2iocseg  23579  0rrv  23654  dmgmseqn0  23696  erdsze2lem1  23734  erdsze2lem2  23735  txsconlem  23771  cvxpcon  23773  cvxscon  23774  cvmsiota  23808  cvmliftiota  23832  cvmlift2lem10  23843  ghomgrp  23997  nobndlem2  24347  nofulllem4  24359  altxpsspw  24511  eleesub  24539  axsegconlem2  24546  axsegconlem8  24552  axlowdimlem7  24576  axlowdimlem17  24586  hfuni  24814  inpws2  25043  fnovrn2  25050  fldrels  25113  isprj2  25164  iscst1  25174  valcurfn1  25204  ppldrels  25227  supdef  25262  supdefa  25263  defge3  25271  inposet  25278  tolat  25286  toplat  25290  unsgrp  25367  trset  25392  ltrset  25402  rltrset  25413  inttop3  25516  qusp  25542  istopxc  25548  limvinlv  25559  conttnf2  25562  exopcopn  25572  prdnei  25573  limptlimpr2lem1  25574  limptlimpr2lem2  25575  islimrs3  25581  islimrs4  25582  bwt2  25592  flfneicn  25625  supbrr  25636  carinttar  25902  prismorcsetlemb  25913  cmpidmor2  25969  isconc1  26006  pgapspf  26052  iscola2  26092  locfindis  26305  tailf  26324  tailfb  26326  supex2g  26419  sdclem1  26453  constcncf  26478  addccncf  26479  sub1cncf  26481  sub2cncf  26482  sstotbnd2  26498  equivbnd2  26516  ismtyres  26532  rrnheibor  26561  reheibor  26563  iccbnd  26564  icccmpALT  26565  exidres  26568  exidresid  26569  mzpnegmpt  26822  vdioph  26859  3anrabdioph  26862  3orrabdioph  26863  rexrabdioph  26875  rexfrabdioph  26876  2rexfrabdioph  26877  3rexfrabdioph  26878  4rexfrabdioph  26879  6rexfrabdioph  26880  7rexfrabdioph  26881  elnnrabdioph  26888  dvdsrabdioph  26891  eldioph4b  26894  pellfundgt1  26968  jm2.27c  27100  lsmfgcl  27172  lmhmfgima  27182  lmhmlnmsplit  27185  pwssplit4  27191  pwslnm  27196  uvcff  27240  frlmsplit2  27243  lindsmm  27298  psgndmsubg  27425  sblpnf  27539  fsumcnf  27692  refsum2cnlem1  27708  fmulcl  27711  itgsinexplem1  27748  stoweidlem2  27751  stoweidlem3  27752  stoweidlem5  27754  stoweidlem20  27769  stoweidlem21  27770  stoweidlem22  27771  stoweidlem23  27772  stoweidlem31  27780  stoweidlem32  27781  stoweidlem35  27784  stoweidlem36  27785  stoweidlem40  27789  stoweidlem41  27790  stoweidlem47  27796  stoweidlem50  27799  stoweidlem57  27806  stoweidlem59  27808  stoweidlem60  27809  stoweidlem62  27811  wallispi2lem2  27821  dp2cl  28239  bnj893  28960  bnj944  28970  bnj969  28978  bnj1136  29027  bnj1177  29036  bnj1452  29082  bnj1489  29086  lshpinN  29179  dalemdea  29851  dalem5  29856  dalem8  29859  dalem9  29861  dalem15  29867  dalem23  29885  cdlemblem  29982  osumcllem1N  30145  osumcllem9N  30153  pexmidlem6N  30164  lhpat2  30234  arglem1N  30379  cdleme0aa  30399  cdleme1b  30415  cdleme1  30416  cdleme2  30417  cdleme3b  30418  cdleme3e  30421  cdleme3h  30424  cdleme7b  30433  cdleme7e  30436  cdleme7ga  30437  cdleme9b  30441  cdleme15d  30466  cdleme22gb  30483  cdlemedb  30486  cdlemeda  30487  cdleme23b  30539  cdleme25cl  30546  cdleme27cl  30555  cdleme29cl  30566  cdlemefs27cl  30602  cdleme42c  30661  cdleme42h  30671  cdleme42i  30672  cdlemg4c  30801  cdlemg4  30806  cdlemg6c  30809  cdlemkvcl  31031  cdlemkoatnle  31040  cdlemk14  31043  cdlemk15  31044  cdlemk29-3  31100  cdlemk37  31103  dia2dimlem1  31254  dvheveccl  31302  diblss  31360  dihglblem5  31488  dih1dimatlem  31519  dihat  31525  dihjatcclem1  31608  dihjatcclem2  31609  dihjatcclem4  31611  dochexmidlem5  31654  dochexmidlem6  31655  lclkrlem2m  31709  lclkrlem2o  31711  lcfrlem3  31734  lcfrlem22  31754  lcfrlem25  31757  lcfrlem30  31762  lcfrlem37  31769  mapdpglem17N  31878  mapdpglem19  31880  hdmap1val  31989
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-cleq 2276  df-clel 2279
  Copyright terms: Public domain W3C validator