MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  snssd Structured version   Visualization version   GIF version

Theorem snssd 4280
Description: The singleton of an element of a class is a subset of the class (deduction rule). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypothesis
Ref Expression
snssd.1 (𝜑𝐴𝐵)
Assertion
Ref Expression
snssd (𝜑 → {𝐴} ⊆ 𝐵)

Proof of Theorem snssd
StepHypRef Expression
1 snssd.1 . 2 (𝜑𝐴𝐵)
2 snssi 4279 . 2 (𝐴𝐵 → {𝐴} ⊆ 𝐵)
31, 2syl 17 1 (𝜑 → {𝐴} ⊆ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  wss 3539  {csn 4124
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-in 3546  df-ss 3553  df-sn 4125
This theorem is referenced by:  sofld  5486  fsnex  6416  fr3nr  6848  wfrlem15  7293  oeeui  7546  ecinxp  7686  ralxpmap  7770  xpdom3  7920  domunsn  7972  mapdom3  7994  isinf  8035  ac6sfi  8066  pwfilem  8120  finsschain  8133  ssfii  8185  marypha1lem  8199  unxpwdom2  8353  en2other2  8692  fseqenlem1  8707  axdc3lem4  9135  axdc4lem  9137  ttukeylem7  9197  fpwwe2lem13  9320  canthwe  9329  canthp1lem1  9330  wuncval2  9425  un0addcl  11173  un0mulcl  11174  ssfzunsn  12212  fseq1p1m1  12238  hashbclem  13045  hashf1lem1  13048  fsumge1  14316  incexclem  14353  isumltss  14365  rpnnen2lem11  14738  bitsinv1  14948  lcmfunsnlem2  15137  lcmfass  15143  phicl2  15257  vdwlem1  15469  vdwlem8  15476  vdwlem12  15480  vdwlem13  15481  0ram  15508  ramub1lem1  15514  ramub1lem2  15515  ramcl  15517  imasaddfnlem  15957  imasaddflem  15959  imasvscafn  15966  imasvscaf  15968  mrieqvlemd  16058  mreexmrid  16072  mreexexlem4d  16076  acsfiindd  16946  acsmapd  16947  gsumress  17045  gsumvallem2  17141  0subg  17388  cycsubg2cl  17401  pmtrprfv  17642  odf1o1  17756  gex1  17775  sylow2alem1  17801  sylow2alem2  17802  lsm01  17853  lsm02  17854  lsmdisj  17863  lsmdisj2  17864  prmcyg  18064  gsumzadd  18091  gsumconst  18103  gsumdifsnd  18129  gsumpt  18130  gsumxp  18144  dmdprdd  18167  dprdfadd  18188  dprdres  18196  dprdz  18198  dprdsn  18204  dprddisj2  18207  dprd2da  18210  dprd2d2  18212  dmdprdsplit2lem  18213  dpjcntz  18220  dpjdisj  18221  dpjlsm  18222  dpjidcl  18226  ablfacrp  18234  ablfac1eu  18241  pgpfac1lem1  18242  pgpfac1lem3a  18244  pgpfac1lem3  18245  pgpfac1lem5  18247  pgpfaclem2  18250  kerf1hrm  18512  lsssn0  18715  lss0ss  18716  lsptpcl  18746  lspsnvsi  18771  lspun0  18778  pwssplit1  18826  lsmpr  18856  lsppr  18860  lspsntri  18864  lspsolvlem  18909  lspsolv  18910  lsppratlem1  18914  lsppratlem3  18916  lsppratlem4  18917  islbs3  18922  lbsextlem4  18928  rsp1  18991  lidlnz  18995  lidldvgen  19022  psrlidm  19170  psrridm  19171  mplmonmul  19231  mulgrhm2  19611  zndvds  19662  mdetdiaglem  20165  mdetrlin  20169  mdetrsca  20170  mdetrsca2  20171  mdetrlin2  20174  mdetunilem5  20183  mdetunilem9  20187  mdetmul  20190  en2top  20542  rest0  20725  ordtrest  20758  iscnp4  20819  cnconst2  20839  cnpdis  20849  ist1-2  20903  cnt1  20906  dishaus  20938  discmp  20953  cmpcld  20957  concompid  20986  dis2ndc  21015  dislly  21052  dissnref  21083  comppfsc  21087  llycmpkgen2  21105  cmpkgen  21106  1stckgenlem  21108  1stckgen  21109  ptbasfi  21136  txdis  21187  txdis1cn  21190  txcmplem1  21196  xkohaus  21208  xkoptsub  21209  xkoinjcn  21242  snfbas  21422  trnei  21448  isufil2  21464  ufileu  21475  filufint  21476  uffixsn  21481  ufildom1  21482  flimopn  21531  hausflim  21537  flimcf  21538  flimclslem  21540  flimsncls  21542  cnpflf2  21556  cnpflf  21557  fclsneii  21573  fclsfnflim  21583  fcfnei  21591  flfcntr  21599  alexsubALTlem3  21605  alexsubALTlem4  21606  ptcmplem2  21609  cldsubg  21666  snclseqg  21671  qustgphaus  21678  tsmsgsum  21694  tsmsid  21695  tgptsmscld  21706  tsmsxplem1  21708  tsmsxplem2  21709  ust0  21775  ustuqtop1  21797  neipcfilu  21852  prdsdsf  21923  prdsxmetlem  21924  prdsmet  21926  imasdsf1olem  21929  xpsdsval  21937  prdsbl  22047  prdsxmslem2  22085  idnghm  22289  icccmplem2  22366  metnrmlem2  22402  ioombl  23057  volivth  23098  itg11  23181  i1fmulclem  23192  itg2mulclem  23236  itgsplitioo  23327  limcvallem  23358  limcdif  23363  ellimc2  23364  limcflf  23368  limcmpt2  23371  limcres  23373  cnplimc  23374  limccnp  23378  limccnp2  23379  limcco  23380  dvreslem  23396  dvaddbr  23424  dvmulbr  23425  dvcmulf  23431  dvef  23464  dvivth  23494  lhop2  23499  lhop  23500  ply1remlem  23643  fta1blem  23649  ig1peu  23652  ig1pdvds  23657  plyco0  23669  elply2  23673  plyf  23675  elplyr  23678  elplyd  23679  ply1term  23681  ply0  23685  plyeq0lem  23687  plyeq0  23688  plypf1  23689  plyaddlem  23692  plymullem  23693  dgrlem  23706  coef2  23708  coeidlem  23714  plyco  23718  coemulhi  23731  plycj  23754  vieta1  23788  taylf  23836  radcnv0  23891  abelth  23916  rlimcnp  24409  xrlimcnp  24412  amgm  24434  wilthlem2  24512  basellem7  24530  basellem9  24532  ppiprm  24594  chtprm  24596  musumsum  24635  muinv  24636  logexprlim  24667  perfectlem2  24672  dchrhash  24713  rpvmasum2  24918  axlowdimlem7  25546  axlowdimlem10  25549  umgraex  25618  umgra1  25621  uslgra1  25667  usgra1  25668  uvtxnm1nbgra  25788  constr1trl  25884  eupa0  26267  eupap1  26269  0oo  26834  sh0le  27489  disjiunel  28597  qtopt1  29036  locfinref  29042  ordtrestNEW  29101  esumsnf  29259  esum2dlem  29287  rossros  29376  oms0  29492  carsggect  29513  eulerpartlems  29555  eulerpartlemgc  29557  eulerpartlemgh  29573  eulerpartlemgs2  29575  plymulx0  29756  bnj1452  30180  subfacp1lem1  30221  subfacp1lem5  30226  erdszelem4  30236  erdszelem8  30240  sconpi1  30281  cvmscld  30315  cvmlift2lem6  30350  cvmlift2lem9  30353  cvmlift2lem11  30355  cvmlift2lem12  30356  mrsubvrs  30479  neibastop2lem  31331  topjoin  31336  fnejoin2  31340  poimirlem3  32378  poimirlem9  32384  poimirlem28  32403  poimirlem32  32407  prdsbnd  32558  heiborlem8  32583  rrnequiv  32600  grpokerinj  32658  0idl  32790  prnc  32832  isfldidl  32833  lshpnel2N  33086  lsatfixedN  33110  lfl0f  33170  lkrlsp3  33205  elpaddatriN  33903  elpaddat  33904  elpadd2at  33906  pmodlem1  33946  osumcllem1N  34056  osumcllem2N  34057  osumcllem9N  34064  osumcllem10N  34065  pexmidlem6N  34075  pexmidlem7N  34076  dibss  35272  dochocsn  35484  dochsncom  35485  dochnel  35496  dihprrnlem1N  35527  dihprrnlem2  35528  djhlsmat  35530  dihsmsprn  35533  dvh4dimlem  35546  dvhdimlem  35547  dochsnnz  35553  dochsatshp  35554  dochsnshp  35556  dochexmid  35571  dochsnkr  35575  dochsnkr2cl  35577  dochfl1  35579  lcfl7lem  35602  lcfl6  35603  lcfl8  35605  lcfl9a  35608  lclkrlem2a  35610  lclkrlem2c  35612  lclkrlem2d  35613  lclkrlem2e  35614  lclkrlem2j  35619  lclkrlem2o  35624  lclkrlem2p  35625  lclkrlem2s  35628  lclkrlem2v  35631  lcfrlem14  35659  lcfrlem18  35663  lcfrlem19  35664  lcfrlem20  35665  lcfrlem23  35668  lcfrlem25  35670  lcdlkreqN  35725  mapdval4N  35735  mapdsn  35744  mapdhvmap  35872  hdmaprnlem4tN  35958  hdmapinvlem1  36024  hdmapinvlem2  36025  hdmapinvlem3  36026  hdmapinvlem4  36027  hdmapglem5  36028  hgmapvvlem3  36031  hdmapglem7a  36033  hdmapglem7b  36034  hdmapglem7  36035  hdmapoc  36037  elrfi  36071  cmpfiiin  36074  mzpcompact2lem  36128  dfac11  36446  pwssplit4  36473  rngunsnply  36558  flcidc  36559  acsfn1p  36584  proot1mul  36592  iocinico  36612  iunrelexp0  36809  frege81d  36854  k0004lem3  37263  binomcxplemnn0  37366  fsumsplit1  38436  islptre  38483  limciccioolb  38485  limcicciooub  38501  limcresiooub  38506  limcresioolb  38507  ioccncflimc  38568  icccncfext  38570  icocncflimc  38572  cncfiooicc  38577  dvnprodlem2  38634  dirkercncflem2  38794  dirkercncflem3  38795  fourierdlem48  38844  fourierdlem49  38845  fourierdlem79  38875  fourierdlem101  38897  sge0sup  39081  hoidmvlelem2  39283  hoiqssbl  39312  hspmbllem1  39313  hspmbllem2  39314  ovnovollem1  39343  perfectALTVlem2  39963  fsumsplitsndif  40215  upgrex  40313  upgr1elem  40332  uvtxanm1nbgr  40626  1hegrlfgr  40717  umgr2v2e  40736  gsumdifsndf  41932
  Copyright terms: Public domain W3C validator