Theorem snssd 4720

Description: The singleton of an element of a class is a subset of the class (deduction form). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypothesis

Ref	Expression
snssd.1	⊢ (𝜑 → 𝐴 ∈ 𝐵)

Assertion

Ref	Expression
snssd	⊢ (𝜑 → {𝐴} ⊆ 𝐵)

Proof of Theorem snssd

Step	Hyp	Ref	Expression
1		snssd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		snssi 4719	. 2 ⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → {𝐴} ⊆ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2121   ⊆ wss 3884  {csn 4557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-ss 3901  df-sn 4558

This theorem is referenced by:  intidg  5398  sofld  6141  fsnex  7230  fr3nr  7718  resf1extb  7878  resf1ext2b  7879  frrlem13  8241  oeeui  8532  naddunif  8623  naddasslem1  8624  naddasslem2  8625  ecinxp  8733  ralxpmap  8838  xpdom3  9007  domunsn  9059  mapdom3  9081  isinf  9169  ac6sfi  9188  pwfilem  9222  finsschain  9263  ssfii  9326  marypha1lem  9340  unxpwdom2  9497  en2other2  9926  fseqenlem1  9941  axdc3lem4  10371  axdc4lem  10373  ttukeylem7  10433  fpwwe2lem12  10561  canthwe  10570  canthp1lem1  10571  wuncval2  10666  un0addcl  12465  un0mulcl  12466  ssfzunsnext  13518  fseq1p1m1  13547  hashbclem  14409  hashf1lem1  14412  fsumsplit1  15702  fsumge1  15755  incexclem  15796  isumltss  15808  fprodsplit1f  15950  rpnnen2lem11  16186  bitsinv1  16406  lcmfunsnlem2  16604  lcmfass  16610  phicl2  16733  vdwlem1  16947  vdwlem8  16954  vdwlem12  16958  vdwlem13  16959  0ram  16986  ramub1lem1  16992  ramub1lem2  16993  ramcl  16995  imasaddfnlem  17487  imasaddflem  17489  imasvscafn  17496  imasvscaf  17498  mrieqvlemd  17590  mreexmrid  17604  mreexexlem4d  17608  acsfiindd  18514  acsmapd  18515  chnccat  18587  gsumress  18645  0subm  18780  gsumvallem2  18797  trivsubgd  19123  trivsubgsnd  19124  trivnsgd  19142  cycsubg2cl  19181  kerf1ghm  19216  pmtrprfv  19422  odf1o1  19541  gex1  19560  sylow2alem1  19586  sylow2alem2  19587  lsm01  19640  lsm02  19641  lsmdisj  19650  lsmdisj2  19651  prmcyg  19863  gsumzadd  19891  gsumconst  19903  gsumdifsnd  19930  gsumpt  19931  gsumxp  19945  dmdprdd  19970  dprdfadd  19991  dprdres  19999  dprdz  20001  dprdsn  20007  dprddisj2  20010  dprd2da  20013  dprd2d2  20015  dmdprdsplit2lem  20016  dpjcntz  20023  dpjdisj  20024  dpjlsm  20025  dpjidcl  20029  ablfacrp  20037  ablfac1eu  20044  pgpfac1lem1  20045  pgpfac1lem3a  20047  pgpfac1lem3  20048  pgpfac1lem5  20050  pgpfaclem2  20053  acsfn1p  20774  lsssn0  20941  lss0ss  20942  lsptpcl  20972  lspsnvsi  20997  lspun0  21004  pwssplit1  21052  lsmpr  21082  lsppr  21086  lspsntri  21090  lspsolvlem  21138  lspsolv  21139  lsppratlem1  21143  lsppratlem3  21145  lsppratlem4  21146  islbs3  21151  lbsextlem4  21157  rnglidl0  21225  rsp1  21233  lidlnz  21238  lidldvgen  21330  mulgrhm2  21456  zndvds  21527  psrlidm  21939  psrridm  21940  mplmonmul  22015  selvvvval  22121  mdetdiaglem  22584  mdetrlin  22588  mdetrsca  22589  mdetrsca2  22590  mdetrlin2  22593  mdetunilem5  22602  mdetunilem9  22606  mdetmul  22609  en2top  22971  rest0  23155  ordtrest  23188  iscnp4  23249  cnconst2  23269  cnpdis  23279  ist1-2  23333  cnt1  23336  dishaus  23368  discmp  23384  cmpcld  23388  conncompid  23417  dis2ndc  23446  dislly  23483  dissnref  23514  comppfsc  23518  llycmpkgen2  23536  cmpkgen  23537  1stckgenlem  23539  1stckgen  23540  ptbasfi  23567  txdis  23618  txdis1cn  23621  txcmplem1  23627  xkohaus  23639  xkoptsub  23640  xkoinjcn  23673  snfbas  23852  trnei  23878  isufil2  23894  ufileu  23905  filufint  23906  uffixsn  23911  ufildom1  23912  flimopn  23961  hausflim  23967  flimcf  23968  flimclslem  23970  flimsncls  23972  cnpflf2  23986  cnpflf  23987  fclsneii  24003  fclsfnflim  24013  fcfnei  24021  flfcntr  24029  alexsubALTlem3  24035  alexsubALTlem4  24036  ptcmplem2  24039  cldsubg  24097  snclseqg  24102  qustgphaus  24109  tsmsgsum  24125  tsmsid  24126  tgptsmscld  24137  tsmsxplem1  24139  tsmsxplem2  24140  ust0  24206  ustuqtop1  24227  neipcfilu  24281  prdsdsf  24353  prdsxmetlem  24354  prdsmet  24356  imasdsf1olem  24359  xpsdsval  24367  prdsbl  24477  prdsxmslem2  24515  idnghm  24729  icccmplem2  24810  metnrmlem2  24847  ioombl  25553  volivth  25595  itg11  25679  i1fmulclem  25690  itg2mulclem  25734  itgsplitioo  25826  limcvallem  25859  limcdif  25864  ellimc2  25865  limcflf  25869  limcmpt2  25872  limcres  25874  cnplimc  25875  limccnp  25879  limccnp2  25880  limcco  25881  dvreslem  25897  dvaddbr  25926  dvmulbr  25927  dvcmulf  25933  dvef  25968  dvivth  25998  lhop2  26003  lhop  26004  ply1remlem  26151  fta1blem  26157  ig1peu  26161  ig1pdvds  26166  plyco0  26178  elply2  26182  plyf  26184  elplyr  26187  elplyd  26188  ply1term  26190  ply0  26194  plyeq0lem  26196  plyeq0  26197  plypf1  26198  plyaddlem  26201  plymullem  26202  dgrlem  26215  coef2  26217  coeidlem  26223  plyco  26227  coemulhi  26240  plycj  26263  plycjOLD  26265  vieta1  26299  taylf  26347  radcnv0  26402  abelth  26427  rlimcnp  26950  xrlimcnp  26953  amgm  26975  wilthlem2  27053  basellem7  27071  basellem9  27073  ppiprm  27135  chtprm  27137  musumsum  27176  muinv  27177  logexprlim  27209  perfectlem2  27214  dchrhash  27255  rpvmasum2  27496  sltssnb  27781  conway  27791  lesrec  27811  eqcuts3  27816  cofcutr  27936  cutlt  27944  cutmax  27946  cutmin  27947  cutminmax  27948  addsuniflem  28013  negsunif  28067  sltmuls1  28159  sltmuls2  28160  precsexlem11  28229  oncutlt  28276  n0fincut  28367  bdaypw2n0bndlem  28475  axlowdimlem7  29037  axlowdimlem10  29040  upgrex  29181  upgr1elem  29201  uvtxnm1nbgr  29493  umgr2v2e  29614  cyclnumvtx  29888  0oo  30880  sh0le  31531  disjiunel  32687  preimane  32763  fnpreimac  32764  fsuppinisegfi  32781  fprodeq02  32918  indsn  32944  s1f1  33024  gsumzresunsn  33145  gsumhashmul  33150  pmtrcnelor  33174  primefldgen1  33407  dvdsrspss  33472  elgrplsmsn  33475  lsmsnorb  33476  grplsm0l  33488  grplsmid  33489  0ringidl  33506  unitpidl1  33509  elrspunsn  33514  drngidl  33518  isprmidlc  33532  qsidomlem2  33538  ssdifidlprm  33543  mxidlprm  33555  mxidlirredi  33556  mxidlirred  33557  drngmxidl  33562  drngmxidlr  33563  qsdrngilem  33579  dflringlem  33587  rsprprmprmidl  33615  rprmirredb  33625  1arithufdlem4  33640  selvply1rhmlem1  33714  selvply1rhmlem2  33715  selvply1rhmlem4  33717  selvply1rhmlem5  33718  selvply1rhm  33719  selvply1rhm0  33720  mvrvalind  33732  mplmulmvr  33733  evlextv  33736  psrmonmul  33744  esplyfval0  33758  esplyfvaln  33768  esplyind  33769  esplyindfv  33770  vietalem  33773  lsatdim  33811  drngdimgt0  33812  dimkerim  33821  evls1fldgencl  33864  algextdeglem1  33911  algextdeglem2  33912  algextdeglem3  33913  algextdeglem4  33914  algextdeglem5  33915  rtelextdg2  33921  constrextdg2lem  33942  constrext2chnlem  33944  constrfiss  33945  qtopt1  34029  locfinref  34035  zarcls0  34062  zarmxt1  34074  zarcmplem  34075  ordtrestNEW  34115  esumsnf  34258  esum2dlem  34286  rossros  34374  oms0  34491  carsggect  34512  eulerpartlems  34554  eulerpartlemgc  34556  eulerpartlemgh  34572  eulerpartlemgs2  34574  plymulx0  34741  circlemeth  34834  hgt750lemb  34850  hgt750leme  34852  bnj1452  35247  pthhashvtx  35369  subfacp1lem1  35420  subfacp1lem5  35425  erdszelem4  35435  erdszelem8  35439  sconnpi1  35480  cvmscld  35514  cvmlift2lem6  35549  cvmlift2lem9  35552  cvmlift2lem11  35554  cvmlift2lem12  35555  mrsubvrs  35763  ellcsrspsn  35882  neibastop2lem  36601  topjoin  36606  fnejoin2  36610  weiunse  36709  pibt2  37792  lindsadd  37993  poimirlem3  38003  poimirlem9  38009  poimirlem28  38028  poimirlem32  38032  prdsbnd  38173  heiborlem8  38198  rrnequiv  38215  grpokerinj  38273  0idl  38405  prnc  38447  isfldidl  38448  lshpnel2N  39490  lsatfixedN  39514  lfl0f  39574  lkrlsp3  39609  elpaddatriN  40308  elpaddat  40309  elpadd2at  40311  pmodlem1  40351  osumcllem1N  40461  osumcllem2N  40462  osumcllem9N  40469  osumcllem10N  40470  pexmidlem6N  40480  pexmidlem7N  40481  dibss  41674  dochocsn  41886  dochsncom  41887  dochnel  41898  dihprrnlem1N  41929  dihprrnlem2  41930  djhlsmat  41932  dihsmsprn  41935  dvh4dimlem  41948  dvhdimlem  41949  dochsnnz  41955  dochsatshp  41956  dochsnshp  41958  dochexmid  41973  dochsnkr  41977  dochsnkr2cl  41979  dochfl1  41981  lcfl7lem  42004  lcfl6  42005  lcfl8  42007  lcfl9a  42010  lclkrlem2a  42012  lclkrlem2c  42014  lclkrlem2d  42015  lclkrlem2e  42016  lclkrlem2j  42021  lclkrlem2o  42026  lclkrlem2p  42027  lclkrlem2s  42030  lclkrlem2v  42033  lcfrlem14  42061  lcfrlem18  42065  lcfrlem19  42066  lcfrlem20  42067  lcfrlem23  42070  lcfrlem25  42072  lcdlkreqN  42127  mapdval4N  42137  mapdsn  42146  mapdhvmap  42274  hdmaprnlem4tN  42357  hdmapinvlem1  42423  hdmapinvlem2  42424  hdmapinvlem3  42425  hdmapinvlem4  42426  hdmapglem5  42427  hgmapvvlem3  42430  hdmapglem7a  42432  hdmapglem7b  42433  hdmapglem7  42434  hdmapoc  42436  aks6d1c5lem3  42635  deg1gprod  42638  sticksstones9  42652  sticksstones11  42654  rhmqusspan  42683  evlsbagval  43049  0prjspnrel  43090  elrfi  43156  cmpfiiin  43159  mzpcompact2lem  43213  dfac11  43520  pwssplit4  43547  rngunsnply  43627  flcidc  43628  proot1mul  43652  iocinico  43670  cantnfresb  43782  iunrelexp0  44159  frege81d  44204  k0004lem3  44606  mnuunid  44734  binomcxplemnn0  44806  islptre  46076  limciccioolb  46078  limcicciooub  46092  limcresiooub  46097  limcresioolb  46098  ioccncflimc  46340  icccncfext  46342  icocncflimc  46344  cncfiooicc  46349  dvnprodlem2  46402  dirkercncflem2  46559  dirkercncflem3  46560  fourierdlem48  46609  fourierdlem49  46610  fourierdlem79  46640  fourierdlem101  46662  sge0sup  46846  hoidmvlelem2  47051  hoiqssbl  47080  hspmbllem1  47081  hspmbllem2  47082  ovnovollem1  47111  fsumsplitsndif  47856  imaelsetpreimafv  47882  perfectALTVlem2  48225  stgrclnbgr0  48468  isubgr3stgrlem3  48471  1hegrlfgr  48635  gsumdifsndf  48684  sepfsepc  49430  discsubc  49566  iinfconstbas  49568