Theorem snssd 4758

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

Syntax hints:   → wi 4   ∈ wcel 2111   ⊆ wss 3897  {csn 4573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3914  df-sn 4574

This theorem is referenced by:  intidg  5396  sofld  6134  fsnex  7217  fr3nr  7705  resf1extb  7864  resf1ext2b  7865  frrlem13  8228  oeeui  8517  naddunif  8608  naddasslem1  8609  naddasslem2  8610  ecinxp  8716  ralxpmap  8820  xpdom3  8988  domunsn  9040  mapdom3  9062  isinf  9149  ac6sfi  9168  pwfilem  9202  finsschain  9243  ssfii  9303  marypha1lem  9317  unxpwdom2  9474  en2other2  9900  fseqenlem1  9915  axdc3lem4  10344  axdc4lem  10346  ttukeylem7  10406  fpwwe2lem12  10533  canthwe  10542  canthp1lem1  10543  wuncval2  10638  un0addcl  12414  un0mulcl  12415  ssfzunsnext  13469  fseq1p1m1  13498  hashbclem  14359  hashf1lem1  14362  fsumsplit1  15652  fsumge1  15704  incexclem  15743  isumltss  15755  fprodsplit1f  15897  rpnnen2lem11  16133  bitsinv1  16353  lcmfunsnlem2  16551  lcmfass  16557  phicl2  16679  vdwlem1  16893  vdwlem8  16900  vdwlem12  16904  vdwlem13  16905  0ram  16932  ramub1lem1  16938  ramub1lem2  16939  ramcl  16941  imasaddfnlem  17432  imasaddflem  17434  imasvscafn  17441  imasvscaf  17443  mrieqvlemd  17535  mreexmrid  17549  mreexexlem4d  17553  acsfiindd  18459  acsmapd  18460  chnccat  18532  gsumress  18590  0subm  18725  gsumvallem2  18742  trivsubgd  19065  trivsubgsnd  19066  trivnsgd  19084  cycsubg2cl  19123  kerf1ghm  19159  pmtrprfv  19365  odf1o1  19484  gex1  19503  sylow2alem1  19529  sylow2alem2  19530  lsm01  19583  lsm02  19584  lsmdisj  19593  lsmdisj2  19594  prmcyg  19806  gsumzadd  19834  gsumconst  19846  gsumdifsnd  19873  gsumpt  19874  gsumxp  19888  dmdprdd  19913  dprdfadd  19934  dprdres  19942  dprdz  19944  dprdsn  19950  dprddisj2  19953  dprd2da  19956  dprd2d2  19958  dmdprdsplit2lem  19959  dpjcntz  19966  dpjdisj  19967  dpjlsm  19968  dpjidcl  19972  ablfacrp  19980  ablfac1eu  19987  pgpfac1lem1  19988  pgpfac1lem3a  19990  pgpfac1lem3  19991  pgpfac1lem5  19993  pgpfaclem2  19996  acsfn1p  20714  lsssn0  20881  lss0ss  20882  lsptpcl  20912  lspsnvsi  20937  lspun0  20944  pwssplit1  20993  lsmpr  21023  lsppr  21027  lspsntri  21031  lspsolvlem  21079  lspsolv  21080  lsppratlem1  21084  lsppratlem3  21086  lsppratlem4  21087  islbs3  21092  lbsextlem4  21098  rnglidl0  21166  rsp1  21174  lidlnz  21179  lidldvgen  21271  mulgrhm2  21415  zndvds  21486  psrlidm  21899  psrridm  21900  mplmonmul  21971  mdetdiaglem  22513  mdetrlin  22517  mdetrsca  22518  mdetrsca2  22519  mdetrlin2  22522  mdetunilem5  22531  mdetunilem9  22535  mdetmul  22538  en2top  22900  rest0  23084  ordtrest  23117  iscnp4  23178  cnconst2  23198  cnpdis  23208  ist1-2  23262  cnt1  23265  dishaus  23297  discmp  23313  cmpcld  23317  conncompid  23346  dis2ndc  23375  dislly  23412  dissnref  23443  comppfsc  23447  llycmpkgen2  23465  cmpkgen  23466  1stckgenlem  23468  1stckgen  23469  ptbasfi  23496  txdis  23547  txdis1cn  23550  txcmplem1  23556  xkohaus  23568  xkoptsub  23569  xkoinjcn  23602  snfbas  23781  trnei  23807  isufil2  23823  ufileu  23834  filufint  23835  uffixsn  23840  ufildom1  23841  flimopn  23890  hausflim  23896  flimcf  23897  flimclslem  23899  flimsncls  23901  cnpflf2  23915  cnpflf  23916  fclsneii  23932  fclsfnflim  23942  fcfnei  23950  flfcntr  23958  alexsubALTlem3  23964  alexsubALTlem4  23965  ptcmplem2  23968  cldsubg  24026  snclseqg  24031  qustgphaus  24038  tsmsgsum  24054  tsmsid  24055  tgptsmscld  24066  tsmsxplem1  24068  tsmsxplem2  24069  ust0  24135  ustuqtop1  24156  neipcfilu  24210  prdsdsf  24282  prdsxmetlem  24283  prdsmet  24285  imasdsf1olem  24288  xpsdsval  24296  prdsbl  24406  prdsxmslem2  24444  idnghm  24658  icccmplem2  24739  metnrmlem2  24776  ioombl  25493  volivth  25535  itg11  25619  i1fmulclem  25630  itg2mulclem  25674  itgsplitioo  25766  limcvallem  25799  limcdif  25804  ellimc2  25805  limcflf  25809  limcmpt2  25812  limcres  25814  cnplimc  25815  limccnp  25819  limccnp2  25820  limcco  25821  dvreslem  25837  dvaddbr  25867  dvmulbr  25868  dvmulbrOLD  25869  dvcmulf  25875  dvef  25911  dvivth  25942  lhop2  25947  lhop  25948  ply1remlem  26097  fta1blem  26103  ig1peu  26107  ig1pdvds  26112  plyco0  26124  elply2  26128  plyf  26130  elplyr  26133  elplyd  26134  ply1term  26136  ply0  26140  plyeq0lem  26142  plyeq0  26143  plypf1  26144  plyaddlem  26147  plymullem  26148  dgrlem  26161  coef2  26163  coeidlem  26169  plyco  26173  coemulhi  26186  plycj  26210  plycjOLD  26212  vieta1  26247  taylf  26295  radcnv0  26352  abelth  26378  rlimcnp  26902  xrlimcnp  26905  amgm  26928  wilthlem2  27006  basellem7  27024  basellem9  27026  ppiprm  27088  chtprm  27090  musumsum  27129  muinv  27130  logexprlim  27163  perfectlem2  27168  dchrhash  27209  rpvmasum2  27450  ssltsnb  27732  slerec  27760  eqscut3  27765  cofcutr  27868  cutlt  27876  cutmax  27878  cutmin  27879  addsuniflem  27944  negsunif  27997  ssltmul1  28086  ssltmul2  28087  precsexlem11  28155  onscutlt  28201  n0sfincut  28282  0reno  28399  axlowdimlem7  28926  axlowdimlem10  28929  upgrex  29070  upgr1elem  29090  uvtxnm1nbgr  29382  umgr2v2e  29504  cyclnumvtx  29778  0oo  30769  sh0le  31420  disjiunel  32576  preimane  32652  fnpreimac  32653  fsuppinisegfi  32668  fprodeq02  32806  s1f1  32924  gsumzresunsn  33036  gsumhashmul  33041  pmtrcnelor  33060  primefldgen1  33287  dvdsrspss  33352  elgrplsmsn  33355  lsmsnorb  33356  grplsm0l  33368  grplsmid  33369  0ringidl  33386  unitpidl1  33389  elrspunsn  33394  drngidl  33398  isprmidlc  33412  qsidomlem2  33418  ssdifidlprm  33423  mxidlprm  33435  mxidlirredi  33436  mxidlirred  33437  drngmxidl  33442  drngmxidlr  33443  qsdrngilem  33459  rsprprmprmidl  33487  rprmirredb  33497  1arithufdlem4  33512  lsatdim  33630  drngdimgt0  33631  dimkerim  33640  evls1fldgencl  33683  algextdeglem1  33730  algextdeglem2  33731  algextdeglem3  33732  algextdeglem4  33733  algextdeglem5  33734  rtelextdg2  33740  constrextdg2lem  33761  constrext2chnlem  33763  constrfiss  33764  qtopt1  33848  locfinref  33854  zarcls0  33881  zarmxt1  33893  zarcmplem  33894  ordtrestNEW  33934  esumsnf  34077  esum2dlem  34105  rossros  34193  oms0  34310  carsggect  34331  eulerpartlems  34373  eulerpartlemgc  34375  eulerpartlemgh  34391  eulerpartlemgs2  34393  plymulx0  34560  circlemeth  34653  hgt750lemb  34669  hgt750leme  34671  bnj1452  35064  pthhashvtx  35172  subfacp1lem1  35223  subfacp1lem5  35228  erdszelem4  35238  erdszelem8  35242  sconnpi1  35283  cvmscld  35317  cvmlift2lem6  35352  cvmlift2lem9  35355  cvmlift2lem11  35357  cvmlift2lem12  35358  mrsubvrs  35566  ellcsrspsn  35685  neibastop2lem  36404  topjoin  36409  fnejoin2  36413  weiunse  36512  pibt2  37461  lindsadd  37663  poimirlem3  37673  poimirlem9  37679  poimirlem28  37698  poimirlem32  37702  prdsbnd  37843  heiborlem8  37868  rrnequiv  37885  grpokerinj  37943  0idl  38075  prnc  38117  isfldidl  38118  lshpnel2N  39094  lsatfixedN  39118  lfl0f  39178  lkrlsp3  39213  elpaddatriN  39912  elpaddat  39913  elpadd2at  39915  pmodlem1  39955  osumcllem1N  40065  osumcllem2N  40066  osumcllem9N  40073  osumcllem10N  40074  pexmidlem6N  40084  pexmidlem7N  40085  dibss  41278  dochocsn  41490  dochsncom  41491  dochnel  41502  dihprrnlem1N  41533  dihprrnlem2  41534  djhlsmat  41536  dihsmsprn  41539  dvh4dimlem  41552  dvhdimlem  41553  dochsnnz  41559  dochsatshp  41560  dochsnshp  41562  dochexmid  41577  dochsnkr  41581  dochsnkr2cl  41583  dochfl1  41585  lcfl7lem  41608  lcfl6  41609  lcfl8  41611  lcfl9a  41614  lclkrlem2a  41616  lclkrlem2c  41618  lclkrlem2d  41619  lclkrlem2e  41620  lclkrlem2j  41625  lclkrlem2o  41630  lclkrlem2p  41631  lclkrlem2s  41634  lclkrlem2v  41637  lcfrlem14  41665  lcfrlem18  41669  lcfrlem19  41670  lcfrlem20  41671  lcfrlem23  41674  lcfrlem25  41676  lcdlkreqN  41731  mapdval4N  41741  mapdsn  41750  mapdhvmap  41878  hdmaprnlem4tN  41961  hdmapinvlem1  42027  hdmapinvlem2  42028  hdmapinvlem3  42029  hdmapinvlem4  42030  hdmapglem5  42031  hgmapvvlem3  42034  hdmapglem7a  42036  hdmapglem7b  42037  hdmapglem7  42038  hdmapoc  42040  aks6d1c5lem3  42240  deg1gprod  42243  sticksstones9  42257  sticksstones11  42259  rhmqusspan  42288  evlsbagval  42669  selvvvval  42688  0prjspnrel  42730  elrfi  42797  cmpfiiin  42800  mzpcompact2lem  42854  dfac11  43165  pwssplit4  43192  rngunsnply  43272  flcidc  43273  proot1mul  43297  iocinico  43315  cantnfresb  43427  iunrelexp0  43805  frege81d  43850  k0004lem3  44252  mnuunid  44380  binomcxplemnn0  44452  islptre  45729  limciccioolb  45731  limcicciooub  45745  limcresiooub  45750  limcresioolb  45751  ioccncflimc  45993  icccncfext  45995  icocncflimc  45997  cncfiooicc  46002  dvnprodlem2  46055  dirkercncflem2  46212  dirkercncflem3  46213  fourierdlem48  46262  fourierdlem49  46263  fourierdlem79  46293  fourierdlem101  46315  sge0sup  46499  hoidmvlelem2  46704  hoiqssbl  46733  hspmbllem1  46734  hspmbllem2  46735  ovnovollem1  46764  fsumsplitsndif  47483  imaelsetpreimafv  47505  perfectALTVlem2  47832  stgrclnbgr0  48075  isubgr3stgrlem3  48078  1hegrlfgr  48242  gsumdifsndf  48291  sepfsepc  49038  discsubc  49175  iinfconstbas  49177