Theorem snssi 4811

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 2107   ⊆ wss 3948  {csn 4628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3955  df-ss 3965  df-sn 4629

This theorem is referenced by:  snssd  4812  difsnid  4813  eldifeldifsn  4814  pwpw0  4816  sssn  4829  ssunsn2  4830  tpssi  4839  pwsnOLD  4901  snelpwiOLD  5444  intidOLD  5458  frirr  5653  xpsspw  5808  djussxp  5844  dmressnsn  6022  fconst6g  6778  f1sng  6873  dffv2  6984  fvimacnvi  7051  fvimacnvALT  7056  fsn2  7131  fsnunf  7180  abnexg  7740  ordsuci  7793  sucexeloniOLD  7795  suceloniOLD  7797  curry1  8087  curry2  8090  xpord2pred  8128  xpord3pred  8135  ressuppss  8165  ressuppssdif  8167  naddcllem  8672  naddov2  8675  mapsnd  8877  ralxpmap  8887  sucdom2OLD  9079  fodomr  9125  findcard2  9161  findcard2s  9162  unfi  9169  ssfi  9170  sucdom2  9203  0sdom1dom  9235  en1eqsnOLD  9272  enp1ilem  9275  findcard2OLD  9281  marypha1lem  9425  marypha2lem1  9427  epfrs  9723  dfac5lem4  10118  kmlem11  10152  ackbij1lem2  10213  fin23lem26  10317  isfin1-3  10378  hsmexlem4  10421  axdc3lem4  10445  axresscn  11140  nn0ssre  12473  nn0sscn  12474  xrsupss  13285  supxrmnf  13293  1exp  14054  hashxrcl  14314  hashdifsn  14371  hashdifsnp1  14454  repsdf2  14725  modfsummods  15736  fsum00  15741  incexc  15780  2ebits  16385  bitsinvp1  16387  lcmfunsnlem2lem1  16572  lcmfunsnlem2lem2  16573  lcmfunsnlem2  16574  coprmproddvdslem  16596  4sqlem19  16893  ramxrcl  16947  mrcsncl  17553  acsfn1  17602  homaf  17977  dmcoass  18013  lubel  18464  gsumws1  18716  eqg0subgecsn  19069  cycsubg2  19082  cntzsnval  19183  0frgp  19642  dpjidcl  19923  ablfac1eu  19938  lspsncl  20581  lspsnss  20594  lspsnid  20597  lpival  20876  lpiss  20881  lidldvgen  20886  znlidl  21077  frlmlbs  21344  mat1dimelbas  21965  smadiadetglem2  22166  isneip  22601  neips  22609  opnneip  22615  maxlp  22643  restsn2  22667  leordtval2  22708  ist1-3  22845  ordtt1  22875  2ndcdisj2  22953  uffix  23417  neiflim  23470  ptcmplem5  23552  cnextfres1  23564  haustsms2  23633  ust0  23716  ustuqtop5  23742  dscopn  24074  icccmplem1  24330  bndth  24466  ovolsn  25004  icombl1  25072  plyun0  25703  coeeulem  25730  coeeu  25731  vieta1lem2  25816  aalioulem2  25838  taylfval  25863  perfectlem2  26723  noextend  27159  noextendseq  27160  conway  27290  etasslt  27304  0slt1s  27320  ssltleft  27355  ssltright  27356  negsid  27505  precsexlem8  27650  precsexlem11  27653  istrkg2ld  27701  axlowdimlem7  28196  axlowdimlem10  28199  0clwlkv  29374  hsn0elch  30489  chsupsn  30654  chsup0  30789  h1deoi  30790  h1dei  30791  h1did  30792  h1de2ctlem  30796  h1de2ci  30797  spansni  30798  spansnch  30801  elspansncl  30806  spansnpji  30819  spanunsni  30820  spanpr  30821  h1datomi  30822  spansnji  30887  h1da  31590  atom1d  31594  superpos  31595  disjun0  31814  djussxp2  31861  mptprop  31908  pwrssmgc  32158  1fldgenq  32401  rspsnid  32474  lindssn  32483  elrspunidl  32535  lbslsat  32690  esumnul  33035  esumcst  33050  hashf2  33071  esum2d  33080  measvuni  33201  cntnevol  33215  eulerpartlemt  33359  eulerpartlemmf  33363  eulerpartlemgh  33366  ballotlemfp1  33479  reprinfz1  33623  fineqvac  34086  f1resfz0f1d  34092  dfon2lem3  34746  altxpsspw  34938  bj-snglss  35840  lindsadd  36470  lindsenlbs  36472  poimirlem16  36493  poimirlem19  36496  poimirlem23  36500  poimirlem25  36502  poimirlem29  36506  poimirlem31  36508  mblfinlem2  36515  dvasin  36561  fdc  36602  prnc  36924  isfldidl  36925  ispridlc  36927  islshpsm  37839  snatpsubN  38610  polatN  38791  atpsubclN  38805  pclfinclN  38810  mapfzcons  41440  mzpcompact2lem  41475  diophrw  41483  brfvidRP  42425  cotrcltrcl  42462  corcltrcl  42476  cotrclrcl  42479  gneispa  42867  binomcxplemnotnn0  43101  snelpwrVD  43578  disjiun2  43731  infxrpnf  44143  mccllem  44300  islptre  44322  cncfdmsn  44593  snmbl  44666  stoweidlem44  44747  sge0tsms  45083  sge0iunmptlemfi  45116  ismeannd  45170  isomenndlem  45233  hoidmvlelem3  45300  hoidmvlelem4  45301  ovnhoilem1  45304  fnbrafvb  45849  afvres  45867  afv2res  45934  perfectALTVlem2  46377  mapsnop  46974  lincext2  47090  snlindsntorlem  47105  aacllem  47802