Theorem snssi 4812

Description: The singleton of an element of a class is a subset of the class. (Contributed by NM, 6-Jun-1994.)

Assertion

Ref	Expression
snssi	⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵)

Proof of Theorem snssi

Step	Hyp	Ref	Expression
1		snssg 4787	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))
2	1	ibi 267	1 ⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2105   ⊆ wss 3962  {csn 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-ss 3979  df-sn 4631

This theorem is referenced by:  snssd  4813  difsnid  4814  eldifeldifsn  4815  pwpw0  4817  sssn  4830  ssunsn2  4831  tpssi  4842  snelpwiOLD  5454  intidOLD  5468  frirr  5664  xpsspw  5821  djussxp  5858  dmressnsn  6042  fconst6g  6797  f1sng  6890  dffv2  7003  fvimacnvi  7071  fvimacnvALT  7076  fsn2  7155  fsnunf  7204  abnexg  7774  ordsuci  7827  sucexeloniOLD  7829  suceloniOLD  7831  curry1  8127  curry2  8130  xpord2pred  8168  xpord3pred  8175  ressuppss  8206  ressuppssdif  8208  naddcllem  8712  naddov2  8715  mapsnd  8924  ralxpmap  8934  sucdom2OLD  9120  fodomr  9166  findcard2  9202  findcard2s  9203  unfi  9209  ssfi  9211  sucdom2  9240  0sdom1dom  9271  en1eqsnOLD  9306  enp1ilem  9309  fodomfir  9365  marypha1lem  9470  marypha2lem1  9472  epfrs  9768  dfac5lem4  10163  dfac5lem4OLD  10165  kmlem11  10198  ackbij1lem2  10257  fin23lem26  10362  isfin1-3  10423  hsmexlem4  10466  axdc3lem4  10490  axresscn  11185  nn0ssre  12527  nn0sscn  12528  xrsupss  13347  supxrmnf  13355  1exp  14128  hashxrcl  14392  hashdifsn  14449  hashdifsnp1  14541  repsdf2  14812  modfsummods  15825  fsum00  15830  incexc  15869  2ebits  16480  bitsinvp1  16482  lcmfunsnlem2lem1  16671  lcmfunsnlem2lem2  16672  lcmfunsnlem2  16673  coprmproddvdslem  16695  4sqlem19  16996  ramxrcl  17050  mrcsncl  17656  acsfn1  17705  homaf  18083  dmcoass  18119  lubel  18571  gsumws1  18863  eqg0subgecsn  19227  cycsubg2  19240  cntzsnval  19354  0frgp  19811  dpjidcl  20092  ablfac1eu  20107  lspsncl  20992  lspsnss  21005  lspsnid  21008  lpival  21351  lpiss  21356  lidldvgen  21361  pzriprnglem10  21518  znlidl  21565  frlmlbs  21834  mat1dimelbas  22492  smadiadetglem2  22693  isneip  23128  neips  23136  opnneip  23142  maxlp  23170  restsn2  23194  leordtval2  23235  ist1-3  23372  ordtt1  23402  2ndcdisj2  23480  uffix  23944  neiflim  23997  ptcmplem5  24079  cnextfres1  24091  haustsms2  24160  ust0  24243  ustuqtop5  24269  dscopn  24601  icccmplem1  24857  bndth  25003  ovolsn  25543  icombl1  25611  plyun0  26250  coeeulem  26277  coeeu  26278  vieta1lem2  26367  aalioulem2  26389  taylfval  26414  perfectlem2  27288  noextend  27725  noextendseq  27726  conway  27858  etasslt  27872  0slt1s  27888  ssltleft  27923  ssltright  27924  negsid  28087  precsexlem8  28252  precsexlem11  28255  n0sbday  28368  nohalf  28421  pw2bday  28432  istrkg2ld  28482  axlowdimlem7  28977  axlowdimlem10  28980  0clwlkv  30159  hsn0elch  31276  chsupsn  31441  chsup0  31576  h1deoi  31577  h1dei  31578  h1did  31579  h1de2ctlem  31583  h1de2ci  31584  spansni  31585  spansnch  31588  elspansncl  31593  spansnpji  31606  spanunsni  31607  spanpr  31608  h1datomi  31609  spansnji  31674  h1da  32377  atom1d  32381  superpos  32382  disjun0  32614  djussxp2  32664  mptprop  32712  pwrssmgc  32974  gsumwrd2dccatlem  33051  1fldgenq  33303  rspsnid  33378  lindssn  33385  elrspunidl  33435  lbslsat  33643  esumnul  34028  esumcst  34043  hashf2  34064  esum2d  34073  measvuni  34194  cntnevol  34208  eulerpartlemt  34352  eulerpartlemmf  34356  eulerpartlemgh  34359  ballotlemfp1  34472  reprinfz1  34615  fineqvac  35089  f1resfz0f1d  35097  dfon2lem3  35766  altxpsspw  35958  bj-snglss  36952  lindsadd  37599  lindsenlbs  37601  poimirlem16  37622  poimirlem19  37625  poimirlem23  37629  poimirlem25  37631  poimirlem29  37635  poimirlem31  37637  mblfinlem2  37644  dvasin  37690  fdc  37731  prnc  38053  isfldidl  38054  ispridlc  38056  islshpsm  38961  snatpsubN  39732  polatN  39913  atpsubclN  39927  pclfinclN  39932  readvrec2  42369  mapfzcons  42703  mzpcompact2lem  42738  diophrw  42746  brfvidRP  43677  cotrcltrcl  43714  corcltrcl  43728  cotrclrcl  43731  gneispa  44119  binomcxplemnotnn0  44351  snelpwrVD  44828  disjiun2  44997  infxrpnf  45395  mccllem  45552  islptre  45574  cncfdmsn  45845  snmbl  45918  stoweidlem44  45999  sge0tsms  46335  sge0iunmptlemfi  46368  ismeannd  46422  isomenndlem  46485  hoidmvlelem3  46552  hoidmvlelem4  46553  ovnhoilem1  46556  fnbrafvb  47103  afvres  47121  afv2res  47188  perfectALTVlem2  47646  mapsnop  48188  lincext2  48300  snlindsntorlem  48315  aacllem  49031