Theorem snssi 4833

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 4808	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))
2	1	ibi 267	1 ⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3976  {csn 4648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-sn 4649

This theorem is referenced by:  snssd  4834  difsnid  4835  eldifeldifsn  4836  pwpw0  4838  sssn  4851  ssunsn2  4852  tpssi  4863  snelpwiOLD  5464  intidOLD  5478  frirr  5676  xpsspw  5833  djussxp  5870  dmressnsn  6052  fconst6g  6810  f1sng  6904  dffv2  7017  fvimacnvi  7085  fvimacnvALT  7090  fsn2  7170  fsnunf  7219  abnexg  7791  ordsuci  7844  sucexeloniOLD  7846  suceloniOLD  7848  curry1  8145  curry2  8148  xpord2pred  8186  xpord3pred  8193  ressuppss  8224  ressuppssdif  8226  naddcllem  8732  naddov2  8735  mapsnd  8944  ralxpmap  8954  sucdom2OLD  9148  fodomr  9194  findcard2  9230  findcard2s  9231  unfi  9238  ssfi  9240  sucdom2  9269  0sdom1dom  9301  en1eqsnOLD  9337  enp1ilem  9340  fodomfir  9396  marypha1lem  9502  marypha2lem1  9504  epfrs  9800  dfac5lem4  10195  dfac5lem4OLD  10197  kmlem11  10230  ackbij1lem2  10289  fin23lem26  10394  isfin1-3  10455  hsmexlem4  10498  axdc3lem4  10522  axresscn  11217  nn0ssre  12557  nn0sscn  12558  xrsupss  13371  supxrmnf  13379  1exp  14142  hashxrcl  14406  hashdifsn  14463  hashdifsnp1  14555  repsdf2  14826  modfsummods  15841  fsum00  15846  incexc  15885  2ebits  16493  bitsinvp1  16495  lcmfunsnlem2lem1  16685  lcmfunsnlem2lem2  16686  lcmfunsnlem2  16687  coprmproddvdslem  16709  4sqlem19  17010  ramxrcl  17064  mrcsncl  17670  acsfn1  17719  homaf  18097  dmcoass  18133  lubel  18584  gsumws1  18873  eqg0subgecsn  19237  cycsubg2  19250  cntzsnval  19364  0frgp  19821  dpjidcl  20102  ablfac1eu  20117  lspsncl  20998  lspsnss  21011  lspsnid  21014  lpival  21357  lpiss  21362  lidldvgen  21367  pzriprnglem10  21524  znlidl  21571  frlmlbs  21840  mat1dimelbas  22498  smadiadetglem2  22699  isneip  23134  neips  23142  opnneip  23148  maxlp  23176  restsn2  23200  leordtval2  23241  ist1-3  23378  ordtt1  23408  2ndcdisj2  23486  uffix  23950  neiflim  24003  ptcmplem5  24085  cnextfres1  24097  haustsms2  24166  ust0  24249  ustuqtop5  24275  dscopn  24607  icccmplem1  24863  bndth  25009  ovolsn  25549  icombl1  25617  plyun0  26256  coeeulem  26283  coeeu  26284  vieta1lem2  26371  aalioulem2  26393  taylfval  26418  perfectlem2  27292  noextend  27729  noextendseq  27730  conway  27862  etasslt  27876  0slt1s  27892  ssltleft  27927  ssltright  27928  negsid  28091  precsexlem8  28256  precsexlem11  28259  n0sbday  28372  nohalf  28425  pw2bday  28436  istrkg2ld  28486  axlowdimlem7  28981  axlowdimlem10  28984  0clwlkv  30163  hsn0elch  31280  chsupsn  31445  chsup0  31580  h1deoi  31581  h1dei  31582  h1did  31583  h1de2ctlem  31587  h1de2ci  31588  spansni  31589  spansnch  31592  elspansncl  31597  spansnpji  31610  spanunsni  31611  spanpr  31612  h1datomi  31613  spansnji  31678  h1da  32381  atom1d  32385  superpos  32386  disjun0  32617  djussxp2  32666  mptprop  32710  pwrssmgc  32973  1fldgenq  33289  rspsnid  33364  lindssn  33371  elrspunidl  33421  lbslsat  33629  esumnul  34012  esumcst  34027  hashf2  34048  esum2d  34057  measvuni  34178  cntnevol  34192  eulerpartlemt  34336  eulerpartlemmf  34340  eulerpartlemgh  34343  ballotlemfp1  34456  reprinfz1  34599  fineqvac  35073  f1resfz0f1d  35081  dfon2lem3  35749  altxpsspw  35941  bj-snglss  36936  lindsadd  37573  lindsenlbs  37575  poimirlem16  37596  poimirlem19  37599  poimirlem23  37603  poimirlem25  37605  poimirlem29  37609  poimirlem31  37611  mblfinlem2  37618  dvasin  37664  fdc  37705  prnc  38027  isfldidl  38028  ispridlc  38030  islshpsm  38936  snatpsubN  39707  polatN  39888  atpsubclN  39902  pclfinclN  39907  mapfzcons  42672  mzpcompact2lem  42707  diophrw  42715  brfvidRP  43650  cotrcltrcl  43687  corcltrcl  43701  cotrclrcl  43704  gneispa  44092  binomcxplemnotnn0  44325  snelpwrVD  44802  disjiun2  44960  infxrpnf  45361  mccllem  45518  islptre  45540  cncfdmsn  45811  snmbl  45884  stoweidlem44  45965  sge0tsms  46301  sge0iunmptlemfi  46334  ismeannd  46388  isomenndlem  46451  hoidmvlelem3  46518  hoidmvlelem4  46519  ovnhoilem1  46522  fnbrafvb  47069  afvres  47087  afv2res  47154  perfectALTVlem2  47596  mapsnop  48069  lincext2  48184  snlindsntorlem  48199  aacllem  48895