Theorem snssi 4738

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

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3883  {csn 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-sn 4559

This theorem is referenced by:  snssd  4739  difsnid  4740  eldifeldifsn  4741  pwpw0  4743  sssn  4756  ssunsn2  4757  tpssi  4766  pwsnOLD  4829  snelpwi  5354  intid  5367  frirr  5557  xpsspw  5708  djussxp  5743  dmressnsn  5922  fconst6g  6647  f1sng  6741  dffv2  6845  fvimacnvi  6911  fvimacnvALT  6916  fsn2  6990  fsnunf  7039  abnexg  7584  suceloni  7635  curry1  7915  curry2  7918  ressuppss  7970  ressuppssdif  7972  mapsnd  8632  ralxpmap  8642  sucdom2  8822  fodomr  8864  findcard2  8909  findcard2s  8910  unfi  8917  ssfi  8918  en1eqsn  8977  enp1ilem  8981  findcard2OLD  8986  marypha1lem  9122  marypha2lem1  9124  epfrs  9420  dfac5lem4  9813  kmlem11  9847  ackbij1lem2  9908  fin23lem26  10012  isfin1-3  10073  hsmexlem4  10116  axdc3lem4  10140  axresscn  10835  nn0ssre  12167  nn0sscn  12168  xrsupss  12972  supxrmnf  12980  1exp  13740  hashxrcl  14000  hashdifsn  14057  hashdifsnp1  14138  repsdf2  14419  modfsummods  15433  fsum00  15438  incexc  15477  2ebits  16082  bitsinvp1  16084  lcmfunsnlem2lem1  16271  lcmfunsnlem2lem2  16272  lcmfunsnlem2  16273  coprmproddvdslem  16295  4sqlem19  16592  ramxrcl  16646  mrcsncl  17238  acsfn1  17287  homaf  17661  dmcoass  17697  lubel  18147  gsumws1  18391  cycsubg2  18744  cntzsnval  18845  0frgp  19300  dpjidcl  19576  ablfac1eu  19591  lspsncl  20154  lspsnss  20167  lspsnid  20170  lpival  20429  lpiss  20434  lidldvgen  20439  znlidl  20649  frlmlbs  20914  mat1dimelbas  21528  smadiadetglem2  21729  isneip  22164  neips  22172  opnneip  22178  maxlp  22206  restsn2  22230  leordtval2  22271  ist1-3  22408  ordtt1  22438  2ndcdisj2  22516  uffix  22980  neiflim  23033  ptcmplem5  23115  cnextfres1  23127  haustsms2  23196  ust0  23279  ustuqtop5  23305  dscopn  23635  icccmplem1  23891  bndth  24027  ovolsn  24564  icombl1  24632  plyun0  25263  coeeulem  25290  coeeu  25291  vieta1lem2  25376  aalioulem2  25398  taylfval  25423  perfectlem2  26283  istrkg2ld  26725  axlowdimlem7  27219  axlowdimlem10  27222  0clwlkv  28396  hsn0elch  29511  chsupsn  29676  chsup0  29811  h1deoi  29812  h1dei  29813  h1did  29814  h1de2ctlem  29818  h1de2ci  29819  spansni  29820  spansnch  29823  elspansncl  29828  spansnpji  29841  spanunsni  29842  spanpr  29843  h1datomi  29844  spansnji  29909  h1da  30612  atom1d  30616  superpos  30617  disjun0  30835  djussxp2  30886  mptprop  30933  pwrssmgc  31180  rspsnid  31470  lindssn  31475  elrspunidl  31508  lbslsat  31601  esumnul  31916  esumcst  31931  hashf2  31952  esum2d  31961  measvuni  32082  cntnevol  32096  eulerpartlemt  32238  eulerpartlemmf  32242  eulerpartlemgh  32245  ballotlemfp1  32358  reprinfz1  32502  fineqvac  32966  f1resfz0f1d  32972  dfon2lem3  33667  xpord2pred  33719  xpord3pred  33725  naddcllem  33758  naddov2  33761  noextend  33796  noextendseq  33797  conway  33920  etasslt  33934  0slt1s  33950  ssltleft  33981  ssltright  33982  addscllem1  34058  altxpsspw  34206  bj-snglss  35087  lindsadd  35697  lindsenlbs  35699  poimirlem16  35720  poimirlem19  35723  poimirlem23  35727  poimirlem25  35729  poimirlem29  35733  poimirlem31  35735  mblfinlem2  35742  dvasin  35788  fdc  35830  prnc  36152  isfldidl  36153  ispridlc  36155  islshpsm  36921  snatpsubN  37691  polatN  37872  atpsubclN  37886  pclfinclN  37891  mapfzcons  40454  mzpcompact2lem  40489  diophrw  40497  brfvidRP  41185  cotrcltrcl  41222  corcltrcl  41236  cotrclrcl  41239  gneispa  41629  binomcxplemnotnn0  41863  snelpwrVD  42340  disjiun2  42495  infxrpnf  42876  mccllem  43028  islptre  43050  cncfdmsn  43321  snmbl  43394  stoweidlem44  43475  sge0tsms  43808  sge0iunmptlemfi  43841  ismeannd  43895  isomenndlem  43958  hoidmvlelem3  44025  hoidmvlelem4  44026  ovnhoilem1  44029  fnbrafvb  44533  afvres  44551  afv2res  44618  perfectALTVlem2  45062  mapsnop  45568  lincext2  45684  snlindsntorlem  45699  aacllem  46391