Theorem snssi 4757

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

Syntax hints:   → wi 4   ∈ wcel 2111   ⊆ wss 3897  {csn 4573

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3914  df-sn 4574

This theorem is referenced by:  snssd  4758  difsnid  4759  eldifeldifsn  4760  pwpw0  4762  sssn  4775  ssunsn2  4776  tpssi  4787  frirr  5590  xpsspw  5748  djussxp  5784  dmressnsn  5971  fconst6g  6712  f1sng  6805  dffv2  6917  fvimacnvi  6985  fvimacnvALT  6990  fsn2  7069  fsnunf  7119  abnexg  7689  ordsuci  7741  curry1  8034  curry2  8037  xpord2pred  8075  xpord3pred  8082  ressuppss  8113  ressuppssdif  8115  naddcllem  8591  naddov2  8594  mapsnd  8810  ralxpmap  8820  fodomr  9041  findcard2  9074  findcard2s  9075  unfi  9080  ssfi  9082  sucdom2  9112  0sdom1dom  9130  enp1ilem  9162  fodomfir  9212  marypha1lem  9317  marypha2lem1  9319  epfrs  9621  dfac5lem4  10017  dfac5lem4OLD  10019  kmlem11  10052  ackbij1lem2  10111  fin23lem26  10216  isfin1-3  10277  hsmexlem4  10320  axdc3lem4  10344  axresscn  11039  nn0ssre  12385  nn0sscn  12386  xrsupss  13208  supxrmnf  13216  1exp  13998  hashxrcl  14264  hashdifsn  14321  hashdifsnp1  14413  repsdf2  14685  modfsummods  15700  fsum00  15705  incexc  15744  2ebits  16358  bitsinvp1  16360  lcmfunsnlem2lem1  16549  lcmfunsnlem2lem2  16550  lcmfunsnlem2  16551  coprmproddvdslem  16573  4sqlem19  16875  ramxrcl  16929  mrcsncl  17518  acsfn1  17567  homaf  17937  dmcoass  17973  lubel  18420  gsumws1  18746  eqg0subgecsn  19109  cycsubg2  19122  cntzsnval  19236  0frgp  19691  dpjidcl  19972  ablfac1eu  19987  lspsncl  20910  lspsnss  20923  lspsnid  20926  lpival  21261  lpiss  21266  lidldvgen  21271  pzriprnglem10  21427  znlidl  21470  frlmlbs  21734  mat1dimelbas  22386  smadiadetglem2  22587  isneip  23020  neips  23028  opnneip  23034  maxlp  23062  restsn2  23086  leordtval2  23127  ist1-3  23264  ordtt1  23294  2ndcdisj2  23372  uffix  23836  neiflim  23889  ptcmplem5  23971  cnextfres1  23983  haustsms2  24052  ust0  24135  ustuqtop5  24160  dscopn  24488  icccmplem1  24738  bndth  24884  ovolsn  25423  icombl1  25491  plyun0  26129  coeeulem  26156  coeeu  26157  vieta1lem2  26246  aalioulem2  26268  taylfval  26293  perfectlem2  27168  noextend  27605  noextendseq  27606  conway  27740  etasslt  27754  0slt1s  27773  ssltleft  27815  ssltright  27816  negsid  27983  precsexlem8  28152  precsexlem11  28155  n0sbday  28280  istrkg2ld  28438  axlowdimlem7  28926  axlowdimlem10  28929  0clwlkv  30111  hsn0elch  31228  chsupsn  31393  chsup0  31528  h1deoi  31529  h1dei  31530  h1did  31531  h1de2ctlem  31535  h1de2ci  31536  spansni  31537  spansnch  31540  elspansncl  31545  spansnpji  31558  spanunsni  31559  spanpr  31560  h1datomi  31561  spansnji  31626  h1da  32329  atom1d  32333  superpos  32334  disjun0  32575  djussxp2  32630  mptprop  32679  pwrssmgc  32981  gsumwrd2dccatlem  33046  elrgspnsubrunlem2  33215  1fldgenq  33288  rspsnid  33336  lindssn  33343  elrspunidl  33393  lbslsat  33629  fldextrspunlsplem  33686  esumnul  34061  esumcst  34076  hashf2  34097  esum2d  34106  measvuni  34227  cntnevol  34241  eulerpartlemt  34384  eulerpartlemmf  34388  eulerpartlemgh  34391  ballotlemfp1  34505  reprinfz1  34635  fineqvac  35139  f1resfz0f1d  35158  dfon2lem3  35827  altxpsspw  36021  bj-snglss  37014  lindsadd  37663  lindsenlbs  37665  poimirlem16  37686  poimirlem19  37689  poimirlem23  37693  poimirlem25  37695  poimirlem29  37699  poimirlem31  37701  mblfinlem2  37708  dvasin  37754  fdc  37795  prnc  38117  isfldidl  38118  ispridlc  38120  islshpsm  39089  snatpsubN  39859  polatN  40040  atpsubclN  40054  pclfinclN  40059  readvrec2  42464  mapfzcons  42819  mzpcompact2lem  42854  diophrw  42862  brfvidRP  43791  cotrcltrcl  43828  corcltrcl  43842  cotrclrcl  43845  gneispa  44233  binomcxplemnotnn0  44459  snelpwrVD  44933  disjiun2  45165  infxrpnf  45554  mccllem  45707  islptre  45729  cncfdmsn  45998  snmbl  46071  stoweidlem44  46152  sge0tsms  46488  sge0iunmptlemfi  46521  ismeannd  46575  isomenndlem  46638  hoidmvlelem3  46705  hoidmvlelem4  46706  ovnhoilem1  46709  fnbrafvb  47264  afvres  47282  afv2res  47349  perfectALTVlem2  47832  mapsnop  48454  lincext2  48566  snlindsntorlem  48581  resinsnALT  48983  aacllem  49912