Theorem snssd 4702

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

Syntax hints:   → wi 4   ∈ wcel 2111   ⊆ wss 3881  {csn 4525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-sn 4526

This theorem is referenced by:  sofld  6011  fsnex  7017  fr3nr  7474  wfrlem15  7952  oeeui  8211  ecinxp  8355  ralxpmap  8443  xpdom3  8598  domunsn  8651  mapdom3  8673  isinf  8715  ac6sfi  8746  pwfilem  8802  finsschain  8815  ssfii  8867  marypha1lem  8881  unxpwdom2  9036  en2other2  9420  fseqenlem1  9435  axdc3lem4  9864  axdc4lem  9866  ttukeylem7  9926  fpwwe2lem13  10053  canthwe  10062  canthp1lem1  10063  wuncval2  10158  un0addcl  11918  un0mulcl  11919  ssfzunsnext  12947  fseq1p1m1  12976  hashbclem  13806  hashf1lem1  13809  fsumge1  15144  incexclem  15183  isumltss  15195  fprodsplit1f  15336  rpnnen2lem11  15569  bitsinv1  15781  lcmfunsnlem2  15974  lcmfass  15980  phicl2  16095  vdwlem1  16307  vdwlem8  16314  vdwlem12  16318  vdwlem13  16319  0ram  16346  ramub1lem1  16352  ramub1lem2  16353  ramcl  16355  imasaddfnlem  16793  imasaddflem  16795  imasvscafn  16802  imasvscaf  16804  mrieqvlemd  16892  mreexmrid  16906  mreexexlem4d  16910  acsfiindd  17779  acsmapd  17780  gsumress  17884  0subm  17974  gsumvallem2  17990  0subg  18296  trivsubgd  18297  trivsubgsnd  18298  trivnsgd  18316  cycsubg2cl  18346  pmtrprfv  18573  odf1o1  18689  gex1  18708  sylow2alem1  18734  sylow2alem2  18735  lsm01  18789  lsm02  18790  lsmdisj  18799  lsmdisj2  18800  prmcyg  19007  gsumzadd  19035  gsumconst  19047  gsumdifsnd  19074  gsumpt  19075  gsumxp  19089  dmdprdd  19114  dprdfadd  19135  dprdres  19143  dprdz  19145  dprdsn  19151  dprddisj2  19154  dprd2da  19157  dprd2d2  19159  dmdprdsplit2lem  19160  dpjcntz  19167  dpjdisj  19168  dpjlsm  19169  dpjidcl  19173  ablfacrp  19181  ablfac1eu  19188  pgpfac1lem1  19189  pgpfac1lem3a  19191  pgpfac1lem3  19192  pgpfac1lem5  19194  pgpfaclem2  19197  kerf1ghm  19491  acsfn1p  19571  lsssn0  19712  lss0ss  19713  lsptpcl  19744  lspsnvsi  19769  lspun0  19776  pwssplit1  19824  lsmpr  19854  lsppr  19858  lspsntri  19862  lspsolvlem  19907  lspsolv  19908  lsppratlem1  19912  lsppratlem3  19914  lsppratlem4  19915  islbs3  19920  lbsextlem4  19926  rsp1  19990  lidlnz  19994  lidldvgen  20021  mulgrhm2  20192  zndvds  20241  psrlidm  20641  psrridm  20642  mplmonmul  20704  mdetdiaglem  21203  mdetrlin  21207  mdetrsca  21208  mdetrsca2  21209  mdetrlin2  21212  mdetunilem5  21221  mdetunilem9  21225  mdetmul  21228  en2top  21590  rest0  21774  ordtrest  21807  iscnp4  21868  cnconst2  21888  cnpdis  21898  ist1-2  21952  cnt1  21955  dishaus  21987  discmp  22003  cmpcld  22007  conncompid  22036  dis2ndc  22065  dislly  22102  dissnref  22133  comppfsc  22137  llycmpkgen2  22155  cmpkgen  22156  1stckgenlem  22158  1stckgen  22159  ptbasfi  22186  txdis  22237  txdis1cn  22240  txcmplem1  22246  xkohaus  22258  xkoptsub  22259  xkoinjcn  22292  snfbas  22471  trnei  22497  isufil2  22513  ufileu  22524  filufint  22525  uffixsn  22530  ufildom1  22531  flimopn  22580  hausflim  22586  flimcf  22587  flimclslem  22589  flimsncls  22591  cnpflf2  22605  cnpflf  22606  fclsneii  22622  fclsfnflim  22632  fcfnei  22640  flfcntr  22648  alexsubALTlem3  22654  alexsubALTlem4  22655  ptcmplem2  22658  cldsubg  22716  snclseqg  22721  qustgphaus  22728  tsmsgsum  22744  tsmsid  22745  tgptsmscld  22756  tsmsxplem1  22758  tsmsxplem2  22759  ust0  22825  ustuqtop1  22847  neipcfilu  22902  prdsdsf  22974  prdsxmetlem  22975  prdsmet  22977  imasdsf1olem  22980  xpsdsval  22988  prdsbl  23098  prdsxmslem2  23136  idnghm  23349  icccmplem2  23428  metnrmlem2  23465  ioombl  24169  volivth  24211  itg11  24295  i1fmulclem  24306  itg2mulclem  24350  itgsplitioo  24441  limcvallem  24474  limcdif  24479  ellimc2  24480  limcflf  24484  limcmpt2  24487  limcres  24489  cnplimc  24490  limccnp  24494  limccnp2  24495  limcco  24496  dvreslem  24512  dvaddbr  24541  dvmulbr  24542  dvcmulf  24548  dvef  24583  dvivth  24613  lhop2  24618  lhop  24619  ply1remlem  24763  fta1blem  24769  ig1peu  24772  ig1pdvds  24777  plyco0  24789  elply2  24793  plyf  24795  elplyr  24798  elplyd  24799  ply1term  24801  ply0  24805  plyeq0lem  24807  plyeq0  24808  plypf1  24809  plyaddlem  24812  plymullem  24813  dgrlem  24826  coef2  24828  coeidlem  24834  plyco  24838  coemulhi  24851  plycj  24874  vieta1  24908  taylf  24956  radcnv0  25011  abelth  25036  rlimcnp  25551  xrlimcnp  25554  amgm  25576  wilthlem2  25654  basellem7  25672  basellem9  25674  ppiprm  25736  chtprm  25738  musumsum  25777  muinv  25778  logexprlim  25809  perfectlem2  25814  dchrhash  25855  rpvmasum2  26096  axlowdimlem7  26742  axlowdimlem10  26745  upgrex  26885  upgr1elem  26905  uvtxnm1nbgr  27194  umgr2v2e  27315  0oo  28572  sh0le  29223  disjiunel  30359  preimane  30433  fnpreimac  30434  fsuppinisegfi  30447  fprodeq02  30565  s1f1  30645  gsumzresunsn  30739  gsumhashmul  30741  pmtrcnelor  30785  elgrplsmsn  30998  lsmsnorb  30999  0ringidl  31013  isprmidlc  31031  qsidomlem2  31037  mxidlprm  31048  lsatdim  31103  drngdimgt0  31104  dimkerim  31111  qtopt1  31188  locfinref  31194  zarcls0  31221  zarmxt1  31233  zarcmplem  31234  ordtrestNEW  31274  esumsnf  31433  esum2dlem  31461  rossros  31549  oms0  31665  carsggect  31686  eulerpartlems  31728  eulerpartlemgc  31730  eulerpartlemgh  31746  eulerpartlemgs2  31748  plymulx0  31927  circlemeth  32021  hgt750lemb  32037  hgt750leme  32039  bnj1452  32434  pthhashvtx  32487  subfacp1lem1  32539  subfacp1lem5  32544  erdszelem4  32554  erdszelem8  32558  sconnpi1  32599  cvmscld  32633  cvmlift2lem6  32668  cvmlift2lem9  32671  cvmlift2lem11  32673  cvmlift2lem12  32674  mrsubvrs  32882  frrlem13  33248  slerec  33390  neibastop2lem  33821  topjoin  33826  fnejoin2  33830  pibt2  34834  lindsadd  35050  poimirlem3  35060  poimirlem9  35066  poimirlem28  35085  poimirlem32  35089  prdsbnd  35231  heiborlem8  35256  rrnequiv  35273  grpokerinj  35331  0idl  35463  prnc  35505  isfldidl  35506  lshpnel2N  36281  lsatfixedN  36305  lfl0f  36365  lkrlsp3  36400  elpaddatriN  37099  elpaddat  37100  elpadd2at  37102  pmodlem1  37142  osumcllem1N  37252  osumcllem2N  37253  osumcllem9N  37260  osumcllem10N  37261  pexmidlem6N  37271  pexmidlem7N  37272  dibss  38465  dochocsn  38677  dochsncom  38678  dochnel  38689  dihprrnlem1N  38720  dihprrnlem2  38721  djhlsmat  38723  dihsmsprn  38726  dvh4dimlem  38739  dvhdimlem  38740  dochsnnz  38746  dochsatshp  38747  dochsnshp  38749  dochexmid  38764  dochsnkr  38768  dochsnkr2cl  38770  dochfl1  38772  lcfl7lem  38795  lcfl6  38796  lcfl8  38798  lcfl9a  38801  lclkrlem2a  38803  lclkrlem2c  38805  lclkrlem2d  38806  lclkrlem2e  38807  lclkrlem2j  38812  lclkrlem2o  38817  lclkrlem2p  38818  lclkrlem2s  38821  lclkrlem2v  38824  lcfrlem14  38852  lcfrlem18  38856  lcfrlem19  38857  lcfrlem20  38858  lcfrlem23  38861  lcfrlem25  38863  lcdlkreqN  38918  mapdval4N  38928  mapdsn  38937  mapdhvmap  39065  hdmaprnlem4tN  39148  hdmapinvlem1  39214  hdmapinvlem2  39215  hdmapinvlem3  39216  hdmapinvlem4  39217  hdmapglem5  39218  hgmapvvlem3  39221  hdmapglem7a  39223  hdmapglem7b  39224  hdmapglem7  39225  hdmapoc  39227  0prjspnrel  39613  elrfi  39635  cmpfiiin  39638  mzpcompact2lem  39692  dfac11  40006  pwssplit4  40033  rngunsnply  40117  flcidc  40118  proot1mul  40143  iocinico  40162  iunrelexp0  40403  frege81d  40448  k0004lem3  40852  mnuunid  40985  binomcxplemnn0  41053  fsumsplit1  42214  islptre  42261  limciccioolb  42263  limcicciooub  42279  limcresiooub  42284  limcresioolb  42285  ioccncflimc  42527  icccncfext  42529  icocncflimc  42531  cncfiooicc  42536  dvnprodlem2  42589  dirkercncflem2  42746  dirkercncflem3  42747  fourierdlem48  42796  fourierdlem49  42797  fourierdlem79  42827  fourierdlem101  42849  sge0sup  43030  hoidmvlelem2  43235  hoiqssbl  43264  hspmbllem1  43265  hspmbllem2  43266  ovnovollem1  43295  fsumsplitsndif  43890  imaelsetpreimafv  43912  perfectALTVlem2  44240  1hegrlfgr  44360  gsumdifsndf  44441