Theorem snssi 4557

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

Syntax hints:   → wi 4   ∈ wcel 2164   ⊆ wss 3798  {csn 4397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-v 3416  df-in 3805  df-ss 3812  df-sn 4398

This theorem is referenced by:  snssd  4558  difsnid  4559  eldifeldifsn  4560  pwpw0  4562  sssn  4575  ssunsn2  4576  tpssi  4585  pwsnALT  4651  snelpwi  5133  intid  5147  frirr  5319  xpsspw  5467  djussxp  5500  dmressnsn  5675  fconst6g  6331  f1sng  6419  dffv2  6518  fvimacnvi  6580  fvimacnvALT  6585  fsn2  6653  fsnunf  6707  abnexg  7225  suceloni  7274  curry1  7533  curry2  7536  ressuppss  7578  ressuppssdif  7580  mapsnd  8164  ralxpmap  8174  fodomr  8380  sucdom2  8425  en1eqsn  8459  enp1ilem  8463  findcard2  8469  findcard2s  8470  marypha1lem  8608  marypha2lem1  8610  epfrs  8884  dfac5lem4  9262  kmlem11  9297  ackbij1lem2  9358  fin23lem26  9462  isfin1-3  9523  hsmexlem4  9566  axdc3lem4  9590  axresscn  10285  nn0ssre  11622  nn0sscn  11623  xrsupss  12427  supxrmnf  12435  1exp  13183  hashxrcl  13438  hashdifsn  13491  hashdifsnp1  13567  repsdf2  13894  modfsummods  14899  fsum00  14904  incexc  14943  fprodsplit1f  15093  2ebits  15542  bitsinvp1  15544  lcmfunsnlem2lem1  15724  lcmfunsnlem2lem2  15725  lcmfunsnlem2  15726  coprmproddvdslem  15748  4sqlem19  16038  ramxrcl  16092  mrcsncl  16625  acsfn1  16674  homaf  17032  dmcoass  17068  lubel  17475  gsumws1  17729  cycsubg2  17982  cntzsnval  18107  0frgp  18545  dpjidcl  18811  ablfac1eu  18826  lspsncl  19336  lspsnss  19349  lspsnid  19352  lpival  19606  lpiss  19611  lidldvgen  19616  znlidl  20241  frlmlbs  20503  mat1dimelbas  20645  smadiadetglem2  20847  isneip  21280  neips  21288  opnneip  21294  maxlp  21322  restsn2  21346  leordtval2  21387  ist1-3  21524  ordtt1  21554  2ndcdisj2  21631  uffix  22095  neiflim  22148  ptcmplem5  22230  cnextfres1  22242  haustsms2  22310  ust0  22393  ustuqtop5  22419  dscopn  22748  icccmplem1  22995  bndth  23127  ovolsn  23661  icombl1  23729  plyun0  24352  coeeulem  24379  coeeu  24380  vieta1lem2  24465  aalioulem2  24487  taylfval  24512  perfectlem2  25368  istrkg2ld  25772  axlowdimlem7  26247  axlowdimlem10  26250  0clwlkv  27496  hsn0elch  28649  chsupsn  28816  chsup0  28951  h1deoi  28952  h1dei  28953  h1did  28954  h1de2ctlem  28958  h1de2ci  28959  spansni  28960  spansnch  28963  elspansncl  28968  spansnpji  28981  spanunsni  28982  spanpr  28983  h1datomi  28984  spansnji  29049  h1da  29752  atom1d  29756  superpos  29757  disjun0  29944  esumnul  30644  esumcst  30659  hashf2  30680  esum2d  30689  measvuni  30811  cntnevol  30825  eulerpartlemt  30967  eulerpartlemmf  30971  eulerpartlemgh  30974  ballotlemfp1  31088  reprinfz1  31238  dfon2lem3  32217  noextend  32347  noextendseq  32348  conway  32438  etasslt  32448  altxpsspw  32612  bj-snglss  33473  lindsadd  33939  lindsenlbs  33941  poimirlem16  33962  poimirlem19  33965  poimirlem23  33969  poimirlem25  33971  poimirlem29  33975  poimirlem31  33977  mblfinlem2  33984  dvasin  34032  fdc  34076  prnc  34401  isfldidl  34402  ispridlc  34404  islshpsm  35048  snatpsubN  35818  polatN  35999  atpsubclN  36013  pclfinclN  36018  mapfzcons  38116  mzpcompact2lem  38151  diophrw  38159  brfvidRP  38814  cotrcltrcl  38851  corcltrcl  38865  cotrclrcl  38868  gneispa  39261  binomcxplemnotnn0  39388  snelpwrVD  39878  disjiun2  40036  infxrpnf  40462  mccllem  40617  islptre  40639  cncfdmsn  40891  snmbl  40966  stoweidlem44  41048  sge0tsms  41381  sge0iunmptlemfi  41414  ismeannd  41468  isomenndlem  41531  hoidmvlelem3  41598  hoidmvlelem4  41599  ovnhoilem1  41602  fnbrafvb  42049  afvres  42067  afv2res  42134  perfectALTVlem2  42454  mapsnop  42963  lincext2  43084  snlindsntorlem  43099  aacllem  43436