Theorem snssi 4280

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

Syntax hints:   → wi 4   ∈ wcel 1977   ⊆ wss 3540  {csn 4125

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554  df-sn 4126

This theorem is referenced by:  snssd  4281  difsnid  4282  pwpw0  4284  sssn  4298  ssunsn2  4299  tpssi  4309  pwsnALT  4367  snelpwi  4839  intid  4853  frirr  5015  xpsspw  5156  djussxp  5189  dmressnsn  5358  fconst6g  6007  f1sng  6090  dffv2  6181  fvimacnvi  6239  fvimacnvALT  6244  fsn2  6309  fsnunf  6356  suceloni  6905  curry1  7156  curry2  7159  ressuppss  7201  ressuppssdif  7203  mapsn  7785  ralxpmap  7793  fodomr  7996  sucdom2  8041  en1eqsn  8075  enp1ilem  8079  findcard2  8085  findcard2s  8086  marypha1lem  8222  marypha2lem1  8224  epfrs  8490  dfac5lem4  8832  kmlem11  8865  ackbij1lem2  8926  fin23lem26  9030  isfin1-3  9091  hsmexlem4  9134  axdc3lem4  9158  axresscn  9848  nn0ssre  11173  xrsupss  12011  supxrmnf  12019  1exp  12751  hashxrcl  13010  hashdifsn  13063  brfi1indlem  13133  repsdf2  13376  modfsummods  14366  fsum00  14371  incexc  14408  fprodsplit1f  14560  2ebits  15007  bitsinvp1  15009  lcmfunsnlem2lem1  15189  lcmfunsnlem2lem2  15190  lcmfunsnlem2  15191  coprmproddvdslem  15214  4sqlem19  15505  ramxrcl  15559  strlemor1  15796  mrcsncl  16095  acsfn1  16145  homaf  16503  dmcoass  16539  lubel  16945  gsumws1  17199  cycsubg2  17454  cntzsnval  17580  0frgp  18015  dpjidcl  18280  ablfac1eu  18295  lspsncl  18798  lspsnss  18811  lspsnid  18814  lpival  19066  lpiss  19071  lidldvgen  19076  znlidl  19700  frlmlbs  19955  mat1dimelbas  20096  smadiadetglem2  20297  isneip  20719  neips  20727  opnneip  20733  maxlp  20761  restsn2  20785  leordtval2  20826  ist1-3  20963  ordtt1  20993  2ndcdisj2  21070  uffix  21535  neiflim  21588  ptcmplem5  21670  cnextfres1  21682  haustsms2  21750  ust0  21833  ustuqtop5  21859  dscopn  22188  icccmplem1  22433  bndth  22565  ovolsn  23070  icombl1  23138  plyun0  23757  coeeulem  23784  coeeu  23785  vieta1lem2  23870  aalioulem2  23892  taylfval  23917  perfectlem2  24755  istrkg2ld  25159  axlowdimlem7  25628  axlowdimlem10  25631  konigsberg  26514  hsn0elch  27489  chsupsn  27656  chsup0  27791  h1deoi  27792  h1dei  27793  h1did  27794  h1de2ctlem  27798  h1de2ci  27799  spansni  27800  spansnch  27803  elspansncl  27808  spansnpji  27821  spanunsni  27822  spanpr  27823  h1datomi  27824  spansnji  27889  h1da  28592  atom1d  28596  superpos  28597  disjun0  28790  esumnul  29437  esumcst  29452  hashf2  29473  esum2d  29482  measvuni  29604  cntnevol  29618  eulerpartlemt  29760  eulerpartlemmf  29764  eulerpartlemgh  29767  ballotlemfp1  29880  dfon2lem3  30934  altxpsspw  31254  bj-snglss  32151  lindsenlbs  32574  poimirlem16  32595  poimirlem19  32598  poimirlem23  32602  poimirlem25  32604  poimirlem29  32608  poimirlem31  32610  mblfinlem2  32617  dvasin  32666  fdc  32711  prnc  33036  isfldidl  33037  ispridlc  33039  islshpsm  33285  snatpsubN  34054  polatN  34235  atpsubclN  34249  pclfinclN  34254  mapfzcons  36297  mzpcompact2lem  36332  diophrw  36340  brfvidRP  36999  cotrcltrcl  37036  corcltrcl  37050  cotrclrcl  37053  gneispa  37448  binomcxplemnotnn0  37577  snelpwrVD  38088  disjiun2  38251  mapsnd  38383  mccllem  38664  islptre  38686  cncfdmsn  38776  snmbl  38855  stoweidlem44  38937  sge0tsms  39273  sge0iunmptlemfi  39306  ismeannd  39360  isomenndlem  39420  hoidmvlelem3  39487  hoidmvlelem4  39488  ovnhoilem1  39491  fnbrafvb  39883  afvres  39901  perfectALTVlem2  40165  mapsnop  41916  lincext2  42038  snlindsntorlem  42053  aacllem  42356