Theorem snssi 4741

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3936  {csn 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-in 3943  df-ss 3952  df-sn 4568

This theorem is referenced by:  snssd  4742  difsnid  4743  eldifeldifsn  4744  pwpw0  4746  sssn  4759  ssunsn2  4760  tpssi  4769  pwsnOLD  4831  snelpwi  5337  intid  5350  frirr  5532  xpsspw  5682  djussxp  5716  dmressnsn  5894  fconst6g  6568  f1sng  6656  dffv2  6756  fvimacnvi  6822  fvimacnvALT  6827  fsn2  6898  fsnunf  6947  abnexg  7478  suceloni  7528  curry1  7799  curry2  7802  ressuppss  7849  ressuppssdif  7851  mapsnd  8450  ralxpmap  8460  fodomr  8668  sucdom2  8714  en1eqsn  8748  enp1ilem  8752  findcard2  8758  findcard2s  8759  marypha1lem  8897  marypha2lem1  8899  epfrs  9173  dfac5lem4  9552  kmlem11  9586  ackbij1lem2  9643  fin23lem26  9747  isfin1-3  9808  hsmexlem4  9851  axdc3lem4  9875  axresscn  10570  nn0ssre  11902  nn0sscn  11903  xrsupss  12703  supxrmnf  12711  1exp  13459  hashxrcl  13719  hashdifsn  13776  hashdifsnp1  13855  repsdf2  14140  modfsummods  15148  fsum00  15153  incexc  15192  2ebits  15796  bitsinvp1  15798  lcmfunsnlem2lem1  15982  lcmfunsnlem2lem2  15983  lcmfunsnlem2  15984  coprmproddvdslem  16006  4sqlem19  16299  ramxrcl  16353  mrcsncl  16883  acsfn1  16932  homaf  17290  dmcoass  17326  lubel  17732  gsumws1  18002  cycsubg2  18353  cntzsnval  18454  0frgp  18905  dpjidcl  19180  ablfac1eu  19195  lspsncl  19749  lspsnss  19762  lspsnid  19765  lpival  20018  lpiss  20023  lidldvgen  20028  znlidl  20680  frlmlbs  20941  mat1dimelbas  21080  smadiadetglem2  21281  isneip  21713  neips  21721  opnneip  21727  maxlp  21755  restsn2  21779  leordtval2  21820  ist1-3  21957  ordtt1  21987  2ndcdisj2  22065  uffix  22529  neiflim  22582  ptcmplem5  22664  cnextfres1  22676  haustsms2  22745  ust0  22828  ustuqtop5  22854  dscopn  23183  icccmplem1  23430  bndth  23562  ovolsn  24096  icombl1  24164  plyun0  24787  coeeulem  24814  coeeu  24815  vieta1lem2  24900  aalioulem2  24922  taylfval  24947  perfectlem2  25806  istrkg2ld  26246  axlowdimlem7  26734  axlowdimlem10  26737  0clwlkv  27910  hsn0elch  29025  chsupsn  29190  chsup0  29325  h1deoi  29326  h1dei  29327  h1did  29328  h1de2ctlem  29332  h1de2ci  29333  spansni  29334  spansnch  29337  elspansncl  29342  spansnpji  29355  spanunsni  29356  spanpr  29357  h1datomi  29358  spansnji  29423  h1da  30126  atom1d  30130  superpos  30131  disjun0  30345  mptprop  30434  rspsnid  30937  lindssn  30939  lbslsat  31014  esumnul  31307  esumcst  31322  hashf2  31343  esum2d  31352  measvuni  31473  cntnevol  31487  eulerpartlemt  31629  eulerpartlemmf  31633  eulerpartlemgh  31636  ballotlemfp1  31749  reprinfz1  31893  f1resfz0f1d  32361  dfon2lem3  33030  noextend  33173  noextendseq  33174  conway  33264  etasslt  33274  altxpsspw  33438  bj-snglss  34285  lindsadd  34900  lindsenlbs  34902  poimirlem16  34923  poimirlem19  34926  poimirlem23  34930  poimirlem25  34932  poimirlem29  34936  poimirlem31  34938  mblfinlem2  34945  dvasin  34993  fdc  35035  prnc  35360  isfldidl  35361  ispridlc  35363  islshpsm  36131  snatpsubN  36901  polatN  37082  atpsubclN  37096  pclfinclN  37101  mapfzcons  39362  mzpcompact2lem  39397  diophrw  39405  brfvidRP  40082  cotrcltrcl  40119  corcltrcl  40133  cotrclrcl  40136  gneispa  40529  binomcxplemnotnn0  40737  snelpwrVD  41214  disjiun2  41369  infxrpnf  41770  mccllem  41927  islptre  41949  cncfdmsn  42222  snmbl  42297  stoweidlem44  42378  sge0tsms  42711  sge0iunmptlemfi  42744  ismeannd  42798  isomenndlem  42861  hoidmvlelem3  42928  hoidmvlelem4  42929  ovnhoilem1  42932  fnbrafvb  43402  afvres  43420  afv2res  43487  perfectALTVlem2  43936  mapsnop  44442  lincext2  44559  snlindsntorlem  44574  aacllem  44951