Theorem snssi 4756

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

Syntax hints:   → wi 4   ∈ wcel 2149   ⊆ wss 3913  {csn 4594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-ss 3930  df-sn 4595

This theorem is referenced by:  snssd  4757  difsnid  4780  eldifeldifsn  4781  pwpw0  4783  sssn  4796  ssunsn2  4797  tpssi  4807  frirr  5638  xpsspw  5797  djussxp  5832  dmressnsn  6023  fconst6g  6768  f1sng  6865  dffv2  6977  fvimacnvi  7048  fvimacnvALT  7053  fsn2  7133  fsnunf  7184  abnexg  7755  ordsuci  7807  curry1  8099  curry2  8102  xpord2pred  8141  xpord3pred  8148  ressuppss  8179  ressuppssdif  8181  naddcllem  8662  naddov2  8665  mapsnd  8884  ralxpmap  8894  fodomr  9116  findcard2  9149  findcard2s  9150  unfi  9155  ssfi  9157  sucdom2  9187  0sdom1dom  9206  enp1ilem  9238  fodomfir  9287  marypha1lem  9393  marypha2lem1  9395  epfrs  9700  dfac5lem4  10110  kmlem11  10144  ackbij1lem2  10203  fin23lem26  10309  isfin1-3  10370  hsmexlem4  10413  axdc3lem4  10437  axresscn  11133  nn0ssre  12508  nn0sscn  12509  xrsupss  13335  supxrmnf  13343  1exp  14127  hashxrcl  14393  hashdifsn  14451  hashdifsnp1  14543  repsdf2  14815  modfsummods  15845  fsum00  15850  incexc  15891  2ebits  16505  bitsinvp1  16507  lcmfunsnlem2lem1  16696  lcmfunsnlem2lem2  16697  lcmfunsnlem2  16698  coprmproddvdslem  16720  4sqlem19  17023  ramxrcl  17077  mrcsncl  17668  acsfn1  17717  homaf  18087  dmcoass  18123  lubel  18570  gsumws1  18897  eqg0subgecsn  19268  cycsubg2  19281  cntzsnval  19394  0frgp  19849  dpjidcl  20130  ablfac1eu  20145  lspsncl  21076  lspsnss  21089  lspsnid  21092  rspsnid  21348  lpival  21461  lpiss  21466  lidldvgen  21471  pzriprnglem10  21609  znlidl  21652  frlmlbs  21916  mat1dimelbas  22597  smadiadetglem2  22798  isneip  23231  neips  23239  opnneip  23245  maxlp  23273  restsn2  23297  leordtval2  23338  ist1-3  23475  ordtt1  23505  2ndcdisj2  23583  uffix  24047  neiflim  24100  ptcmplem5  24182  cnextfres1  24194  haustsms2  24263  ust0  24346  ustuqtop5  24371  dscopn  24699  icccmplem1  24949  bndth  25086  ovolsn  25623  icombl1  25691  plyun0  26323  coeeulem  26350  coeeu  26351  vieta1lem2  26441  aalioulem2  26463  taylfval  26488  perfectlem2  27360  noextend  27796  noextendseq  27797  conway  27938  etaslts  27952  0lt1s  27971  sltsleft  28019  sltsright  28020  negsid  28200  precsexlem8  28373  precsexlem11  28376  n0bday  28511  elreno2  28654  istrkg2ld  28695  axlowdimlem7  29239  axlowdimlem10  29242  0clwlkv  30423  hsn0elch  31541  chsupsn  31706  chsup0  31841  h1deoi  31842  h1dei  31843  h1did  31844  h1de2ctlem  31848  h1de2ci  31849  spansni  31850  spansnch  31853  elspansncl  31858  spansnpji  31871  spanunsni  31872  spanpr  31873  h1datomi  31874  spansnji  31939  h1da  32642  atom1d  32646  superpos  32647  disjun0  32881  djussxp2  32934  mptprop  32984  pwrssmgc  33261  gsumwrd2dccatlem  33338  elrgspnsubrunlem2  33509  1fldgenq  33586  lindssn  33635  elrspunidl  33680  esplyfval1  33908  esplyfvaln  33909  lbslsat  33951  fldextrspunlsplem  34008  esumnul  34383  esumcst  34398  hashf2  34419  esum2d  34428  measvuni  34549  cntnevol  34563  eulerpartlemt  34706  eulerpartlemmf  34710  eulerpartlemgh  34713  ballotlemfp1  34827  reprinfz1  34954  fineqvac  35452  f1resfz0f1d  35504  dfon2lem3  36174  altxpsspw  36368  ttcmin  36896  ttcsnmin  36918  bj-snglss  37494  lindsadd  38152  lindsenlbs  38154  poimirlem16  38175  poimirlem19  38178  poimirlem23  38182  poimirlem25  38184  poimirlem29  38188  poimirlem31  38190  mblfinlem2  38197  dvasin  38243  fdc  38284  prnc  38606  isfldidl  38607  ispridlc  38609  islshpsm  39644  snatpsubN  40414  polatN  40595  atpsubclN  40609  pclfinclN  40614  readvrec2  43012  mapfzcons  43339  mzpcompact2lem  43374  diophrw  43382  brfvidRP  44306  cotrcltrcl  44343  corcltrcl  44357  cotrclrcl  44360  gneispa  44748  binomcxplemnotnn0  44958  snelpwrVD  45431  disjiun2  45670  infxrpnf  46052  mccllem  46205  islptre  46227  cncfdmsn  46496  snmbl  46569  stoweidlem44  46650  sge0tsms  46986  sge0iunmptlemfi  47019  ismeannd  47073  isomenndlem  47136  hoidmvlelem3  47203  hoidmvlelem4  47204  ovnhoilem1  47207  fnbrafvb  47780  afvres  47798  afv2res  47865  perfectALTVlem2  48376  mapsnop  49009  lincext2  49120  snlindsntorlem  49135  resinsnALT  49536  aacllem  50475