Theorem snssd 4785

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

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3926  {csn 4601

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-ss 3943  df-sn 4602

This theorem is referenced by:  intidg  5432  sofld  6176  fsnex  7275  fr3nr  7764  resf1extb  7928  resf1ext2b  7929  frrlem13  8295  wfrlem15OLD  8335  oeeui  8612  naddunif  8703  naddasslem1  8704  naddasslem2  8705  ecinxp  8804  ralxpmap  8908  xpdom3  9082  domunsn  9139  mapdom3  9161  isinf  9266  isinfOLD  9267  ac6sfi  9290  pwfilem  9326  finsschain  9369  ssfii  9429  marypha1lem  9443  unxpwdom2  9600  en2other2  10021  fseqenlem1  10036  axdc3lem4  10465  axdc4lem  10467  ttukeylem7  10527  fpwwe2lem12  10654  canthwe  10663  canthp1lem1  10664  wuncval2  10759  un0addcl  12532  un0mulcl  12533  ssfzunsnext  13584  fseq1p1m1  13613  hashbclem  14468  hashf1lem1  14471  fsumsplit1  15759  fsumge1  15811  incexclem  15850  isumltss  15862  fprodsplit1f  16004  rpnnen2lem11  16240  bitsinv1  16459  lcmfunsnlem2  16657  lcmfass  16663  phicl2  16785  vdwlem1  16999  vdwlem8  17006  vdwlem12  17010  vdwlem13  17011  0ram  17038  ramub1lem1  17044  ramub1lem2  17045  ramcl  17047  imasaddfnlem  17540  imasaddflem  17542  imasvscafn  17549  imasvscaf  17551  mrieqvlemd  17639  mreexmrid  17653  mreexexlem4d  17657  acsfiindd  18561  acsmapd  18562  gsumress  18658  0subm  18793  gsumvallem2  18810  0subgOLD  19133  trivsubgd  19134  trivsubgsnd  19135  trivnsgd  19153  cycsubg2cl  19192  kerf1ghm  19228  pmtrprfv  19432  odf1o1  19551  gex1  19570  sylow2alem1  19596  sylow2alem2  19597  lsm01  19650  lsm02  19651  lsmdisj  19660  lsmdisj2  19661  prmcyg  19873  gsumzadd  19901  gsumconst  19913  gsumdifsnd  19940  gsumpt  19941  gsumxp  19955  dmdprdd  19980  dprdfadd  20001  dprdres  20009  dprdz  20011  dprdsn  20017  dprddisj2  20020  dprd2da  20023  dprd2d2  20025  dmdprdsplit2lem  20026  dpjcntz  20033  dpjdisj  20034  dpjlsm  20035  dpjidcl  20039  ablfacrp  20047  ablfac1eu  20054  pgpfac1lem1  20055  pgpfac1lem3a  20057  pgpfac1lem3  20058  pgpfac1lem5  20060  pgpfaclem2  20063  acsfn1p  20757  lsssn0  20903  lss0ss  20904  lsptpcl  20934  lspsnvsi  20959  lspun0  20966  pwssplit1  21015  lsmpr  21045  lsppr  21049  lspsntri  21053  lspsolvlem  21101  lspsolv  21102  lsppratlem1  21106  lsppratlem3  21108  lsppratlem4  21109  islbs3  21114  lbsextlem4  21120  rnglidl0  21188  rsp1  21196  lidlnz  21201  lidldvgen  21293  mulgrhm2  21437  zndvds  21508  psrlidm  21920  psrridm  21921  mplmonmul  21992  mdetdiaglem  22534  mdetrlin  22538  mdetrsca  22539  mdetrsca2  22540  mdetrlin2  22543  mdetunilem5  22552  mdetunilem9  22556  mdetmul  22559  en2top  22921  rest0  23105  ordtrest  23138  iscnp4  23199  cnconst2  23219  cnpdis  23229  ist1-2  23283  cnt1  23286  dishaus  23318  discmp  23334  cmpcld  23338  conncompid  23367  dis2ndc  23396  dislly  23433  dissnref  23464  comppfsc  23468  llycmpkgen2  23486  cmpkgen  23487  1stckgenlem  23489  1stckgen  23490  ptbasfi  23517  txdis  23568  txdis1cn  23571  txcmplem1  23577  xkohaus  23589  xkoptsub  23590  xkoinjcn  23623  snfbas  23802  trnei  23828  isufil2  23844  ufileu  23855  filufint  23856  uffixsn  23861  ufildom1  23862  flimopn  23911  hausflim  23917  flimcf  23918  flimclslem  23920  flimsncls  23922  cnpflf2  23936  cnpflf  23937  fclsneii  23953  fclsfnflim  23963  fcfnei  23971  flfcntr  23979  alexsubALTlem3  23985  alexsubALTlem4  23986  ptcmplem2  23989  cldsubg  24047  snclseqg  24052  qustgphaus  24059  tsmsgsum  24075  tsmsid  24076  tgptsmscld  24087  tsmsxplem1  24089  tsmsxplem2  24090  ust0  24156  ustuqtop1  24178  neipcfilu  24232  prdsdsf  24304  prdsxmetlem  24305  prdsmet  24307  imasdsf1olem  24310  xpsdsval  24318  prdsbl  24428  prdsxmslem2  24466  idnghm  24680  icccmplem2  24761  metnrmlem2  24798  ioombl  25516  volivth  25558  itg11  25642  i1fmulclem  25653  itg2mulclem  25697  itgsplitioo  25789  limcvallem  25822  limcdif  25827  ellimc2  25828  limcflf  25832  limcmpt2  25835  limcres  25837  cnplimc  25838  limccnp  25842  limccnp2  25843  limcco  25844  dvreslem  25860  dvaddbr  25890  dvmulbr  25891  dvmulbrOLD  25892  dvcmulf  25898  dvef  25934  dvivth  25965  lhop2  25970  lhop  25971  ply1remlem  26120  fta1blem  26126  ig1peu  26130  ig1pdvds  26135  plyco0  26147  elply2  26151  plyf  26153  elplyr  26156  elplyd  26157  ply1term  26159  ply0  26163  plyeq0lem  26165  plyeq0  26166  plypf1  26167  plyaddlem  26170  plymullem  26171  dgrlem  26184  coef2  26186  coeidlem  26192  plyco  26196  coemulhi  26209  plycj  26233  plycjOLD  26235  vieta1  26270  taylf  26318  radcnv0  26375  abelth  26401  rlimcnp  26925  xrlimcnp  26928  amgm  26951  wilthlem2  27029  basellem7  27047  basellem9  27049  ppiprm  27111  chtprm  27113  musumsum  27152  muinv  27153  logexprlim  27186  perfectlem2  27191  dchrhash  27232  rpvmasum2  27473  ssltsn  27754  slerec  27781  cofcutr  27875  cutlt  27883  cutmax  27885  cutmin  27886  addsuniflem  27951  negsunif  28004  ssltmul1  28090  ssltmul2  28091  precsexlem11  28158  nohalf  28324  0reno  28346  axlowdimlem7  28873  axlowdimlem10  28876  upgrex  29017  upgr1elem  29037  uvtxnm1nbgr  29329  umgr2v2e  29451  cyclnumvtx  29728  0oo  30716  sh0le  31367  disjiunel  32523  preimane  32594  fnpreimac  32595  fsuppinisegfi  32610  fprodeq02  32748  s1f1  32864  gsumzresunsn  32996  gsumhashmul  33001  pmtrcnelor  33048  primefldgen1  33261  dvdsrspss  33348  elgrplsmsn  33351  lsmsnorb  33352  grplsm0l  33364  grplsmid  33365  0ringidl  33382  unitpidl1  33385  elrspunsn  33390  drngidl  33394  isprmidlc  33408  qsidomlem2  33414  ssdifidlprm  33419  mxidlprm  33431  mxidlirredi  33432  mxidlirred  33433  drngmxidl  33438  drngmxidlr  33439  qsdrngilem  33455  rsprprmprmidl  33483  rprmirredb  33493  1arithufdlem4  33508  lsatdim  33603  drngdimgt0  33604  dimkerim  33613  evls1fldgencl  33657  algextdeglem1  33697  algextdeglem2  33698  algextdeglem3  33699  algextdeglem4  33700  algextdeglem5  33701  rtelextdg2  33707  constrextdg2lem  33728  constrext2chnlem  33730  constrfiss  33731  qtopt1  33812  locfinref  33818  zarcls0  33845  zarmxt1  33857  zarcmplem  33858  ordtrestNEW  33898  esumsnf  34041  esum2dlem  34069  rossros  34157  oms0  34275  carsggect  34296  eulerpartlems  34338  eulerpartlemgc  34340  eulerpartlemgh  34356  eulerpartlemgs2  34358  plymulx0  34525  circlemeth  34618  hgt750lemb  34634  hgt750leme  34636  bnj1452  35029  pthhashvtx  35096  subfacp1lem1  35147  subfacp1lem5  35152  erdszelem4  35162  erdszelem8  35166  sconnpi1  35207  cvmscld  35241  cvmlift2lem6  35276  cvmlift2lem9  35279  cvmlift2lem11  35281  cvmlift2lem12  35282  mrsubvrs  35490  ellcsrspsn  35609  neibastop2lem  36324  topjoin  36329  fnejoin2  36333  weiunse  36432  pibt2  37381  lindsadd  37583  poimirlem3  37593  poimirlem9  37599  poimirlem28  37618  poimirlem32  37622  prdsbnd  37763  heiborlem8  37788  rrnequiv  37805  grpokerinj  37863  0idl  37995  prnc  38037  isfldidl  38038  lshpnel2N  38949  lsatfixedN  38973  lfl0f  39033  lkrlsp3  39068  elpaddatriN  39768  elpaddat  39769  elpadd2at  39771  pmodlem1  39811  osumcllem1N  39921  osumcllem2N  39922  osumcllem9N  39929  osumcllem10N  39930  pexmidlem6N  39940  pexmidlem7N  39941  dibss  41134  dochocsn  41346  dochsncom  41347  dochnel  41358  dihprrnlem1N  41389  dihprrnlem2  41390  djhlsmat  41392  dihsmsprn  41395  dvh4dimlem  41408  dvhdimlem  41409  dochsnnz  41415  dochsatshp  41416  dochsnshp  41418  dochexmid  41433  dochsnkr  41437  dochsnkr2cl  41439  dochfl1  41441  lcfl7lem  41464  lcfl6  41465  lcfl8  41467  lcfl9a  41470  lclkrlem2a  41472  lclkrlem2c  41474  lclkrlem2d  41475  lclkrlem2e  41476  lclkrlem2j  41481  lclkrlem2o  41486  lclkrlem2p  41487  lclkrlem2s  41490  lclkrlem2v  41493  lcfrlem14  41521  lcfrlem18  41525  lcfrlem19  41526  lcfrlem20  41527  lcfrlem23  41530  lcfrlem25  41532  lcdlkreqN  41587  mapdval4N  41597  mapdsn  41606  mapdhvmap  41734  hdmaprnlem4tN  41817  hdmapinvlem1  41883  hdmapinvlem2  41884  hdmapinvlem3  41885  hdmapinvlem4  41886  hdmapglem5  41887  hgmapvvlem3  41890  hdmapglem7a  41892  hdmapglem7b  41893  hdmapglem7  41894  hdmapoc  41896  aks6d1c5lem3  42096  deg1gprod  42099  sticksstones9  42113  sticksstones11  42115  rhmqusspan  42144  evlsbagval  42536  selvvvval  42555  0prjspnrel  42597  elrfi  42664  cmpfiiin  42667  mzpcompact2lem  42721  dfac11  43033  pwssplit4  43060  rngunsnply  43140  flcidc  43141  proot1mul  43165  iocinico  43183  cantnfresb  43295  iunrelexp0  43673  frege81d  43718  k0004lem3  44120  mnuunid  44249  binomcxplemnn0  44321  islptre  45596  limciccioolb  45598  limcicciooub  45614  limcresiooub  45619  limcresioolb  45620  ioccncflimc  45862  icccncfext  45864  icocncflimc  45866  cncfiooicc  45871  dvnprodlem2  45924  dirkercncflem2  46081  dirkercncflem3  46082  fourierdlem48  46131  fourierdlem49  46132  fourierdlem79  46162  fourierdlem101  46184  sge0sup  46368  hoidmvlelem2  46573  hoiqssbl  46602  hspmbllem1  46603  hspmbllem2  46604  ovnovollem1  46633  fsumsplitsndif  47335  imaelsetpreimafv  47357  perfectALTVlem2  47684  stgrclnbgr0  47925  isubgr3stgrlem3  47928  1hegrlfgr  48055  gsumdifsndf  48104  sepfsepc  48850  discsubc  48979  iinfconstbas  48981