Theorem snssi 4808

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

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3951  {csn 4626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-sn 4627

This theorem is referenced by:  snssd  4809  difsnid  4810  eldifeldifsn  4811  pwpw0  4813  sssn  4826  ssunsn2  4827  tpssi  4838  snelpwiOLD  5449  intidOLD  5463  frirr  5661  xpsspw  5819  djussxp  5856  dmressnsn  6041  fconst6g  6797  f1sng  6890  dffv2  7004  fvimacnvi  7072  fvimacnvALT  7077  fsn2  7156  fsnunf  7205  abnexg  7776  ordsuci  7828  sucexeloniOLD  7830  suceloniOLD  7832  curry1  8129  curry2  8132  xpord2pred  8170  xpord3pred  8177  ressuppss  8208  ressuppssdif  8210  naddcllem  8714  naddov2  8717  mapsnd  8926  ralxpmap  8936  sucdom2OLD  9122  fodomr  9168  findcard2  9204  findcard2s  9205  unfi  9211  ssfi  9213  sucdom2  9243  0sdom1dom  9274  en1eqsnOLD  9309  enp1ilem  9312  fodomfir  9368  marypha1lem  9473  marypha2lem1  9475  epfrs  9771  dfac5lem4  10166  dfac5lem4OLD  10168  kmlem11  10201  ackbij1lem2  10260  fin23lem26  10365  isfin1-3  10426  hsmexlem4  10469  axdc3lem4  10493  axresscn  11188  nn0ssre  12530  nn0sscn  12531  xrsupss  13351  supxrmnf  13359  1exp  14132  hashxrcl  14396  hashdifsn  14453  hashdifsnp1  14545  repsdf2  14816  modfsummods  15829  fsum00  15834  incexc  15873  2ebits  16484  bitsinvp1  16486  lcmfunsnlem2lem1  16675  lcmfunsnlem2lem2  16676  lcmfunsnlem2  16677  coprmproddvdslem  16699  4sqlem19  17001  ramxrcl  17055  mrcsncl  17655  acsfn1  17704  homaf  18075  dmcoass  18111  lubel  18559  gsumws1  18851  eqg0subgecsn  19215  cycsubg2  19228  cntzsnval  19342  0frgp  19797  dpjidcl  20078  ablfac1eu  20093  lspsncl  20975  lspsnss  20988  lspsnid  20991  lpival  21334  lpiss  21339  lidldvgen  21344  pzriprnglem10  21501  znlidl  21548  frlmlbs  21817  mat1dimelbas  22477  smadiadetglem2  22678  isneip  23113  neips  23121  opnneip  23127  maxlp  23155  restsn2  23179  leordtval2  23220  ist1-3  23357  ordtt1  23387  2ndcdisj2  23465  uffix  23929  neiflim  23982  ptcmplem5  24064  cnextfres1  24076  haustsms2  24145  ust0  24228  ustuqtop5  24254  dscopn  24586  icccmplem1  24844  bndth  24990  ovolsn  25530  icombl1  25598  plyun0  26236  coeeulem  26263  coeeu  26264  vieta1lem2  26353  aalioulem2  26375  taylfval  26400  perfectlem2  27274  noextend  27711  noextendseq  27712  conway  27844  etasslt  27858  0slt1s  27874  ssltleft  27909  ssltright  27910  negsid  28073  precsexlem8  28238  precsexlem11  28241  n0sbday  28354  nohalf  28407  pw2bday  28418  istrkg2ld  28468  axlowdimlem7  28963  axlowdimlem10  28966  0clwlkv  30150  hsn0elch  31267  chsupsn  31432  chsup0  31567  h1deoi  31568  h1dei  31569  h1did  31570  h1de2ctlem  31574  h1de2ci  31575  spansni  31576  spansnch  31579  elspansncl  31584  spansnpji  31597  spanunsni  31598  spanpr  31599  h1datomi  31600  spansnji  31665  h1da  32368  atom1d  32372  superpos  32373  disjun0  32608  djussxp2  32658  mptprop  32707  pwrssmgc  32990  gsumwrd2dccatlem  33069  elrgspnsubrunlem2  33252  1fldgenq  33324  rspsnid  33399  lindssn  33406  elrspunidl  33456  lbslsat  33667  fldextrspunlsplem  33723  esumnul  34049  esumcst  34064  hashf2  34085  esum2d  34094  measvuni  34215  cntnevol  34229  eulerpartlemt  34373  eulerpartlemmf  34377  eulerpartlemgh  34380  ballotlemfp1  34494  reprinfz1  34637  fineqvac  35111  f1resfz0f1d  35119  dfon2lem3  35786  altxpsspw  35978  bj-snglss  36971  lindsadd  37620  lindsenlbs  37622  poimirlem16  37643  poimirlem19  37646  poimirlem23  37650  poimirlem25  37652  poimirlem29  37656  poimirlem31  37658  mblfinlem2  37665  dvasin  37711  fdc  37752  prnc  38074  isfldidl  38075  ispridlc  38077  islshpsm  38981  snatpsubN  39752  polatN  39933  atpsubclN  39947  pclfinclN  39952  readvrec2  42391  mapfzcons  42727  mzpcompact2lem  42762  diophrw  42770  brfvidRP  43701  cotrcltrcl  43738  corcltrcl  43752  cotrclrcl  43755  gneispa  44143  binomcxplemnotnn0  44375  snelpwrVD  44851  disjiun2  45063  infxrpnf  45457  mccllem  45612  islptre  45634  cncfdmsn  45905  snmbl  45978  stoweidlem44  46059  sge0tsms  46395  sge0iunmptlemfi  46428  ismeannd  46482  isomenndlem  46545  hoidmvlelem3  46612  hoidmvlelem4  46613  ovnhoilem1  46616  fnbrafvb  47166  afvres  47184  afv2res  47251  perfectALTVlem2  47709  mapsnop  48260  lincext2  48372  snlindsntorlem  48387  resinsnALT  48773  aacllem  49320