Theorem snssi 4768

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3911  {csn 4585

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-ss 3928  df-sn 4586

This theorem is referenced by:  snssd  4769  difsnid  4770  eldifeldifsn  4771  pwpw0  4773  sssn  4786  ssunsn2  4787  tpssi  4798  snelpwiOLD  5399  intidOLD  5413  frirr  5607  xpsspw  5763  djussxp  5799  dmressnsn  5983  fconst6g  6731  f1sng  6824  dffv2  6938  fvimacnvi  7006  fvimacnvALT  7011  fsn2  7090  fsnunf  7141  abnexg  7712  ordsuci  7764  sucexeloniOLD  7766  curry1  8060  curry2  8063  xpord2pred  8101  xpord3pred  8108  ressuppss  8139  ressuppssdif  8141  naddcllem  8617  naddov2  8620  mapsnd  8836  ralxpmap  8846  fodomr  9069  findcard2  9105  findcard2s  9106  unfi  9112  ssfi  9114  sucdom2  9144  0sdom1dom  9162  en1eqsnOLD  9196  enp1ilem  9199  fodomfir  9255  marypha1lem  9360  marypha2lem1  9362  epfrs  9660  dfac5lem4  10055  dfac5lem4OLD  10057  kmlem11  10090  ackbij1lem2  10149  fin23lem26  10254  isfin1-3  10315  hsmexlem4  10358  axdc3lem4  10382  axresscn  11077  nn0ssre  12422  nn0sscn  12423  xrsupss  13245  supxrmnf  13253  1exp  14032  hashxrcl  14298  hashdifsn  14355  hashdifsnp1  14447  repsdf2  14719  modfsummods  15735  fsum00  15740  incexc  15779  2ebits  16393  bitsinvp1  16395  lcmfunsnlem2lem1  16584  lcmfunsnlem2lem2  16585  lcmfunsnlem2  16586  coprmproddvdslem  16608  4sqlem19  16910  ramxrcl  16964  mrcsncl  17553  acsfn1  17602  homaf  17972  dmcoass  18008  lubel  18455  gsumws1  18747  eqg0subgecsn  19111  cycsubg2  19124  cntzsnval  19238  0frgp  19693  dpjidcl  19974  ablfac1eu  19989  lspsncl  20915  lspsnss  20928  lspsnid  20931  lpival  21266  lpiss  21271  lidldvgen  21276  pzriprnglem10  21432  znlidl  21475  frlmlbs  21739  mat1dimelbas  22391  smadiadetglem2  22592  isneip  23025  neips  23033  opnneip  23039  maxlp  23067  restsn2  23091  leordtval2  23132  ist1-3  23269  ordtt1  23299  2ndcdisj2  23377  uffix  23841  neiflim  23894  ptcmplem5  23976  cnextfres1  23988  haustsms2  24057  ust0  24140  ustuqtop5  24166  dscopn  24494  icccmplem1  24744  bndth  24890  ovolsn  25429  icombl1  25497  plyun0  26135  coeeulem  26162  coeeu  26163  vieta1lem2  26252  aalioulem2  26274  taylfval  26299  perfectlem2  27174  noextend  27611  noextendseq  27612  conway  27745  etasslt  27759  0slt1s  27778  ssltleft  27819  ssltright  27820  negsid  27987  precsexlem8  28156  precsexlem11  28159  n0sbday  28284  istrkg2ld  28440  axlowdimlem7  28928  axlowdimlem10  28931  0clwlkv  30110  hsn0elch  31227  chsupsn  31392  chsup0  31527  h1deoi  31528  h1dei  31529  h1did  31530  h1de2ctlem  31534  h1de2ci  31535  spansni  31536  spansnch  31539  elspansncl  31544  spansnpji  31557  spanunsni  31558  spanpr  31559  h1datomi  31560  spansnji  31625  h1da  32328  atom1d  32332  superpos  32333  disjun0  32574  djussxp2  32622  mptprop  32671  pwrssmgc  32972  gsumwrd2dccatlem  33049  elrgspnsubrunlem2  33215  1fldgenq  33288  rspsnid  33335  lindssn  33342  elrspunidl  33392  lbslsat  33605  fldextrspunlsplem  33661  esumnul  34031  esumcst  34046  hashf2  34067  esum2d  34076  measvuni  34197  cntnevol  34211  eulerpartlemt  34355  eulerpartlemmf  34359  eulerpartlemgh  34362  ballotlemfp1  34476  reprinfz1  34606  fineqvac  35080  f1resfz0f1d  35094  dfon2lem3  35766  altxpsspw  35958  bj-snglss  36951  lindsadd  37600  lindsenlbs  37602  poimirlem16  37623  poimirlem19  37626  poimirlem23  37630  poimirlem25  37632  poimirlem29  37636  poimirlem31  37638  mblfinlem2  37645  dvasin  37691  fdc  37732  prnc  38054  isfldidl  38055  ispridlc  38057  islshpsm  38966  snatpsubN  39737  polatN  39918  atpsubclN  39932  pclfinclN  39937  readvrec2  42342  mapfzcons  42697  mzpcompact2lem  42732  diophrw  42740  brfvidRP  43670  cotrcltrcl  43707  corcltrcl  43721  cotrclrcl  43724  gneispa  44112  binomcxplemnotnn0  44338  snelpwrVD  44813  disjiun2  45045  infxrpnf  45435  mccllem  45588  islptre  45610  cncfdmsn  45881  snmbl  45954  stoweidlem44  46035  sge0tsms  46371  sge0iunmptlemfi  46404  ismeannd  46458  isomenndlem  46521  hoidmvlelem3  46588  hoidmvlelem4  46589  ovnhoilem1  46592  fnbrafvb  47148  afvres  47166  afv2res  47233  perfectALTVlem2  47716  mapsnop  48325  lincext2  48437  snlindsntorlem  48452  resinsnALT  48854  aacllem  49783