Theorem snssi 4753

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ⊆ wss 3906  {csn 4591

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-ss 3923  df-sn 4592

This theorem is used by:  snssd  4754  difsnid  4778  eldifeldifsn  4779  pwpw0  4781  sssn  4794  ssunsn2  4795  tpssi  4805  frirr  5639  xpsspw  5798  djussxp  5833  dmressnsn  6024  fconst6g  6771  f1sng  6868  dffv2  6980  fvimacnvi  7051  fvimacnvALT  7056  fsn2  7136  fsnunf  7189  abnexg  7761  ordsuci  7813  curry1  8105  curry2  8108  xpord2pred  8147  xpord3pred  8154  ressuppss  8185  ressuppssdif  8187  naddcllem  8668  naddov2  8671  mapsnd  8890  ralxpmap  8900  fodomr  9123  findcard2  9156  findcard2s  9157  unfi  9162  ssfi  9164  sucdom2  9194  0sdom1dom  9213  enp1ilem  9245  fodomfir  9294  marypha1lem  9400  marypha2lem1  9402  epfrs  9707  dfac5lem4  10126  kmlem11  10160  ackbij1lem2  10219  fin23lem26  10324  isfin1-3  10385  hsmexlem4  10428  axdc3lem4  10452  axresscn  11150  nn0ssre  12525  nn0sscn  12526  xrsupss  13353  supxrmnf  13361  f1resfz0f1d  13840  1exp  14147  hashxrcl  14413  hashdifsn  14471  hashdifsnp1  14563  repsdf2  14841  modfsummods  15870  fsum00  15875  incexc  15916  2ebits  16529  bitsinvp1  16531  lcmfunsnlem2lem1  16720  lcmfunsnlem2lem2  16721  lcmfunsnlem2  16722  coprmproddvdslem  16744  4sqlem19  17047  ramxrcl  17101  mrcsncl  17692  acsfn1  17741  homaf  18111  dmcoass  18147  lubel  18594  gsumws1  18936  eqg0subgecsn  19314  cycsubg2  19327  cntzsnval  19440  0frgp  19895  dpjidcl  20176  ablfac1eu  20191  lspsncl  21150  lspsnss  21163  lspsnid  21166  rspsnid  21425  lpival  21544  lpiss  21549  lidldvgen  21554  pzriprnglem10  21692  znlidl  21735  frlmlbs  21999  mat1dimelbas  22680  smadiadetglem2  22881  isneip  23314  neips  23322  opnneip  23328  maxlp  23356  restsn2  23380  leordtval2  23421  ist1-3  23558  ordtt1  23588  2ndcdisj2  23667  uffix  24131  neiflim  24184  ptcmplem5  24266  cnextfres1  24278  haustsms2  24347  ust0  24430  ustuqtop5  24455  dscopn  24783  icccmplem1  25033  bndth  25170  ovolsn  25707  icombl1  25775  plyun0  26407  coeeulem  26434  coeeu  26435  vieta1lem2  26525  aalioulem2  26549  taylfval  26575  perfectlem2  27447  noextend  27883  noextendseq  27884  conway  28025  etaslts  28039  0lt1s  28058  sltsleft  28106  sltsright  28107  negsid  28287  precsexlem8  28460  precsexlem11  28463  n0bday  28598  elreno2  28741  istrkg2ld  28782  axlowdimlem7  29355  axlowdimlem10  29358  0clwlkv  30551  hsn0elch  31673  chsupsn  31838  chsup0  31973  h1deoi  31974  h1dei  31975  h1did  31976  h1de2ctlem  31980  h1de2ci  31981  spansni  31982  spansnch  31985  elspansncl  31990  spansnpji  32003  spanunsni  32004  spanpr  32005  h1datomi  32006  spansnji  32071  h1da  32774  atom1d  32778  superpos  32779  disjun0  33013  djussxp2  33066  mptprop  33116  pwrssmgc  33386  gsumwrd2dccatlem  33463  elrgspnsubrunlem2  33634  1fldgenq  33709  lindssn  33757  elrspunidl  33802  esplyfval1  34029  esplyfvaln  34030  lbslsat  34072  fldextrspunlsplem  34129  esumnul  34504  esumcst  34519  hashf2  34540  esum2d  34549  measvuni  34671  cntnevol  34685  eulerpartlemt  34828  eulerpartlemmf  34832  eulerpartlemgh  34835  ballotlemfp1  34949  reprinfz1  35076  fineqvac  35588  dfon2lem3  36314  altxpsspw  36508  ttcmin  37066  ttcsnmin  37088  bj-snglss  37665  lindsadd  38323  lindsenlbs  38325  poimirlem16  38346  poimirlem19  38349  poimirlem23  38353  poimirlem25  38355  poimirlem29  38359  poimirlem31  38361  mblfinlem2  38368  dvasin  38414  fdc  38456  prnc  38778  isfldidl  38779  ispridlc  38781  islshpsm  39814  snatpsubN  40584  polatN  40765  atpsubclN  40779  pclfinclN  40784  readvrec2  43182  mapfzcons  43507  mzpcompact2lem  43542  diophrw  43550  brfvidRP  44474  cotrcltrcl  44511  corcltrcl  44525  cotrclrcl  44528  gneispa  44916  binomcxplemnotnn0  45126  snelpwrVD  45599  disjiun2  45838  infxrpnf  46220  mccllem  46373  islptre  46395  cncfdmsn  46664  snmbl  46737  stoweidlem44  46818  sge0tsms  47154  sge0iunmptlemfi  47187  ismeannd  47241  isomenndlem  47304  hoidmvlelem3  47371  hoidmvlelem4  47372  ovnhoilem1  47375  fnbrafvb  47951  afvres  47969  afv2res  48036  perfectALTVlem2  48547  mapsnop  49183  lincext2  49294  snlindsntorlem  49309  resinsnALT  49710  aacllem  50680