Theorem snssd 4773

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 4772	. 2 ⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → {𝐴} ⊆ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3914  {csn 4589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-ss 3931  df-sn 4590

This theorem is referenced by:  intidg  5417  sofld  6160  fsnex  7258  fr3nr  7748  resf1extb  7910  resf1ext2b  7911  frrlem13  8277  oeeui  8566  naddunif  8657  naddasslem1  8658  naddasslem2  8659  ecinxp  8765  ralxpmap  8869  xpdom3  9039  domunsn  9091  mapdom3  9113  isinf  9207  isinfOLD  9208  ac6sfi  9231  pwfilem  9267  finsschain  9310  ssfii  9370  marypha1lem  9384  unxpwdom2  9541  en2other2  9962  fseqenlem1  9977  axdc3lem4  10406  axdc4lem  10408  ttukeylem7  10468  fpwwe2lem12  10595  canthwe  10604  canthp1lem1  10605  wuncval2  10700  un0addcl  12475  un0mulcl  12476  ssfzunsnext  13530  fseq1p1m1  13559  hashbclem  14417  hashf1lem1  14420  fsumsplit1  15711  fsumge1  15763  incexclem  15802  isumltss  15814  fprodsplit1f  15956  rpnnen2lem11  16192  bitsinv1  16412  lcmfunsnlem2  16610  lcmfass  16616  phicl2  16738  vdwlem1  16952  vdwlem8  16959  vdwlem12  16963  vdwlem13  16964  0ram  16991  ramub1lem1  16997  ramub1lem2  16998  ramcl  17000  imasaddfnlem  17491  imasaddflem  17493  imasvscafn  17500  imasvscaf  17502  mrieqvlemd  17590  mreexmrid  17604  mreexexlem4d  17608  acsfiindd  18512  acsmapd  18513  gsumress  18609  0subm  18744  gsumvallem2  18761  0subgOLD  19084  trivsubgd  19085  trivsubgsnd  19086  trivnsgd  19104  cycsubg2cl  19143  kerf1ghm  19179  pmtrprfv  19383  odf1o1  19502  gex1  19521  sylow2alem1  19547  sylow2alem2  19548  lsm01  19601  lsm02  19602  lsmdisj  19611  lsmdisj2  19612  prmcyg  19824  gsumzadd  19852  gsumconst  19864  gsumdifsnd  19891  gsumpt  19892  gsumxp  19906  dmdprdd  19931  dprdfadd  19952  dprdres  19960  dprdz  19962  dprdsn  19968  dprddisj2  19971  dprd2da  19974  dprd2d2  19976  dmdprdsplit2lem  19977  dpjcntz  19984  dpjdisj  19985  dpjlsm  19986  dpjidcl  19990  ablfacrp  19998  ablfac1eu  20005  pgpfac1lem1  20006  pgpfac1lem3a  20008  pgpfac1lem3  20009  pgpfac1lem5  20011  pgpfaclem2  20014  acsfn1p  20708  lsssn0  20854  lss0ss  20855  lsptpcl  20885  lspsnvsi  20910  lspun0  20917  pwssplit1  20966  lsmpr  20996  lsppr  21000  lspsntri  21004  lspsolvlem  21052  lspsolv  21053  lsppratlem1  21057  lsppratlem3  21059  lsppratlem4  21060  islbs3  21065  lbsextlem4  21071  rnglidl0  21139  rsp1  21147  lidlnz  21152  lidldvgen  21244  mulgrhm2  21388  zndvds  21459  psrlidm  21871  psrridm  21872  mplmonmul  21943  mdetdiaglem  22485  mdetrlin  22489  mdetrsca  22490  mdetrsca2  22491  mdetrlin2  22494  mdetunilem5  22503  mdetunilem9  22507  mdetmul  22510  en2top  22872  rest0  23056  ordtrest  23089  iscnp4  23150  cnconst2  23170  cnpdis  23180  ist1-2  23234  cnt1  23237  dishaus  23269  discmp  23285  cmpcld  23289  conncompid  23318  dis2ndc  23347  dislly  23384  dissnref  23415  comppfsc  23419  llycmpkgen2  23437  cmpkgen  23438  1stckgenlem  23440  1stckgen  23441  ptbasfi  23468  txdis  23519  txdis1cn  23522  txcmplem1  23528  xkohaus  23540  xkoptsub  23541  xkoinjcn  23574  snfbas  23753  trnei  23779  isufil2  23795  ufileu  23806  filufint  23807  uffixsn  23812  ufildom1  23813  flimopn  23862  hausflim  23868  flimcf  23869  flimclslem  23871  flimsncls  23873  cnpflf2  23887  cnpflf  23888  fclsneii  23904  fclsfnflim  23914  fcfnei  23922  flfcntr  23930  alexsubALTlem3  23936  alexsubALTlem4  23937  ptcmplem2  23940  cldsubg  23998  snclseqg  24003  qustgphaus  24010  tsmsgsum  24026  tsmsid  24027  tgptsmscld  24038  tsmsxplem1  24040  tsmsxplem2  24041  ust0  24107  ustuqtop1  24129  neipcfilu  24183  prdsdsf  24255  prdsxmetlem  24256  prdsmet  24258  imasdsf1olem  24261  xpsdsval  24269  prdsbl  24379  prdsxmslem2  24417  idnghm  24631  icccmplem2  24712  metnrmlem2  24749  ioombl  25466  volivth  25508  itg11  25592  i1fmulclem  25603  itg2mulclem  25647  itgsplitioo  25739  limcvallem  25772  limcdif  25777  ellimc2  25778  limcflf  25782  limcmpt2  25785  limcres  25787  cnplimc  25788  limccnp  25792  limccnp2  25793  limcco  25794  dvreslem  25810  dvaddbr  25840  dvmulbr  25841  dvmulbrOLD  25842  dvcmulf  25848  dvef  25884  dvivth  25915  lhop2  25920  lhop  25921  ply1remlem  26070  fta1blem  26076  ig1peu  26080  ig1pdvds  26085  plyco0  26097  elply2  26101  plyf  26103  elplyr  26106  elplyd  26107  ply1term  26109  ply0  26113  plyeq0lem  26115  plyeq0  26116  plypf1  26117  plyaddlem  26120  plymullem  26121  dgrlem  26134  coef2  26136  coeidlem  26142  plyco  26146  coemulhi  26159  plycj  26183  plycjOLD  26185  vieta1  26220  taylf  26268  radcnv0  26325  abelth  26351  rlimcnp  26875  xrlimcnp  26878  amgm  26901  wilthlem2  26979  basellem7  26997  basellem9  26999  ppiprm  27061  chtprm  27063  musumsum  27102  muinv  27103  logexprlim  27136  perfectlem2  27141  dchrhash  27182  rpvmasum2  27423  ssltsn  27704  slerec  27731  cofcutr  27832  cutlt  27840  cutmax  27842  cutmin  27843  addsuniflem  27908  negsunif  27961  ssltmul1  28050  ssltmul2  28051  precsexlem11  28119  onscutlt  28165  n0sfincut  28246  0reno  28348  axlowdimlem7  28875  axlowdimlem10  28878  upgrex  29019  upgr1elem  29039  uvtxnm1nbgr  29331  umgr2v2e  29453  cyclnumvtx  29730  0oo  30718  sh0le  31369  disjiunel  32525  preimane  32594  fnpreimac  32595  fsuppinisegfi  32610  fprodeq02  32748  s1f1  32864  gsumzresunsn  32996  gsumhashmul  33001  pmtrcnelor  33048  primefldgen1  33271  dvdsrspss  33358  elgrplsmsn  33361  lsmsnorb  33362  grplsm0l  33374  grplsmid  33375  0ringidl  33392  unitpidl1  33395  elrspunsn  33400  drngidl  33404  isprmidlc  33418  qsidomlem2  33424  ssdifidlprm  33429  mxidlprm  33441  mxidlirredi  33442  mxidlirred  33443  drngmxidl  33448  drngmxidlr  33449  qsdrngilem  33465  rsprprmprmidl  33493  rprmirredb  33503  1arithufdlem4  33518  lsatdim  33613  drngdimgt0  33614  dimkerim  33623  evls1fldgencl  33665  algextdeglem1  33707  algextdeglem2  33708  algextdeglem3  33709  algextdeglem4  33710  algextdeglem5  33711  rtelextdg2  33717  constrextdg2lem  33738  constrext2chnlem  33740  constrfiss  33741  qtopt1  33825  locfinref  33831  zarcls0  33858  zarmxt1  33870  zarcmplem  33871  ordtrestNEW  33911  esumsnf  34054  esum2dlem  34082  rossros  34170  oms0  34288  carsggect  34309  eulerpartlems  34351  eulerpartlemgc  34353  eulerpartlemgh  34369  eulerpartlemgs2  34371  plymulx0  34538  circlemeth  34631  hgt750lemb  34647  hgt750leme  34649  bnj1452  35042  pthhashvtx  35115  subfacp1lem1  35166  subfacp1lem5  35171  erdszelem4  35181  erdszelem8  35185  sconnpi1  35226  cvmscld  35260  cvmlift2lem6  35295  cvmlift2lem9  35298  cvmlift2lem11  35300  cvmlift2lem12  35301  mrsubvrs  35509  ellcsrspsn  35628  neibastop2lem  36348  topjoin  36353  fnejoin2  36357  weiunse  36456  pibt2  37405  lindsadd  37607  poimirlem3  37617  poimirlem9  37623  poimirlem28  37642  poimirlem32  37646  prdsbnd  37787  heiborlem8  37812  rrnequiv  37829  grpokerinj  37887  0idl  38019  prnc  38061  isfldidl  38062  lshpnel2N  38978  lsatfixedN  39002  lfl0f  39062  lkrlsp3  39097  elpaddatriN  39797  elpaddat  39798  elpadd2at  39800  pmodlem1  39840  osumcllem1N  39950  osumcllem2N  39951  osumcllem9N  39958  osumcllem10N  39959  pexmidlem6N  39969  pexmidlem7N  39970  dibss  41163  dochocsn  41375  dochsncom  41376  dochnel  41387  dihprrnlem1N  41418  dihprrnlem2  41419  djhlsmat  41421  dihsmsprn  41424  dvh4dimlem  41437  dvhdimlem  41438  dochsnnz  41444  dochsatshp  41445  dochsnshp  41447  dochexmid  41462  dochsnkr  41466  dochsnkr2cl  41468  dochfl1  41470  lcfl7lem  41493  lcfl6  41494  lcfl8  41496  lcfl9a  41499  lclkrlem2a  41501  lclkrlem2c  41503  lclkrlem2d  41504  lclkrlem2e  41505  lclkrlem2j  41510  lclkrlem2o  41515  lclkrlem2p  41516  lclkrlem2s  41519  lclkrlem2v  41522  lcfrlem14  41550  lcfrlem18  41554  lcfrlem19  41555  lcfrlem20  41556  lcfrlem23  41559  lcfrlem25  41561  lcdlkreqN  41616  mapdval4N  41626  mapdsn  41635  mapdhvmap  41763  hdmaprnlem4tN  41846  hdmapinvlem1  41912  hdmapinvlem2  41913  hdmapinvlem3  41914  hdmapinvlem4  41915  hdmapglem5  41916  hgmapvvlem3  41919  hdmapglem7a  41921  hdmapglem7b  41922  hdmapglem7  41923  hdmapoc  41925  aks6d1c5lem3  42125  deg1gprod  42128  sticksstones9  42142  sticksstones11  42144  rhmqusspan  42173  evlsbagval  42554  selvvvval  42573  0prjspnrel  42615  elrfi  42682  cmpfiiin  42685  mzpcompact2lem  42739  dfac11  43051  pwssplit4  43078  rngunsnply  43158  flcidc  43159  proot1mul  43183  iocinico  43201  cantnfresb  43313  iunrelexp0  43691  frege81d  43736  k0004lem3  44138  mnuunid  44266  binomcxplemnn0  44338  islptre  45617  limciccioolb  45619  limcicciooub  45635  limcresiooub  45640  limcresioolb  45641  ioccncflimc  45883  icccncfext  45885  icocncflimc  45887  cncfiooicc  45892  dvnprodlem2  45945  dirkercncflem2  46102  dirkercncflem3  46103  fourierdlem48  46152  fourierdlem49  46153  fourierdlem79  46183  fourierdlem101  46205  sge0sup  46389  hoidmvlelem2  46594  hoiqssbl  46623  hspmbllem1  46624  hspmbllem2  46625  ovnovollem1  46654  fsumsplitsndif  47374  imaelsetpreimafv  47396  perfectALTVlem2  47723  stgrclnbgr0  47964  isubgr3stgrlem3  47967  1hegrlfgr  48120  gsumdifsndf  48169  sepfsepc  48916  discsubc  49053  iinfconstbas  49055