Theorem snssi 4740

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

Syntax hints:   → wi 4   ∈ wcel 2110   ⊆ wss 3935  {csn 4566

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-in 3942  df-ss 3951  df-sn 4567

This theorem is referenced by:  snssd  4741  difsnid  4742  eldifeldifsn  4743  pwpw0  4745  sssn  4758  ssunsn2  4759  tpssi  4768  pwsnALT  4830  snelpwi  5336  intid  5349  frirr  5531  xpsspw  5681  djussxp  5715  dmressnsn  5893  fconst6g  6567  f1sng  6655  dffv2  6755  fvimacnvi  6821  fvimacnvALT  6826  fsn2  6897  fsnunf  6946  abnexg  7477  suceloni  7527  curry1  7798  curry2  7801  ressuppss  7848  ressuppssdif  7850  mapsnd  8449  ralxpmap  8459  fodomr  8667  sucdom2  8713  en1eqsn  8747  enp1ilem  8751  findcard2  8757  findcard2s  8758  marypha1lem  8896  marypha2lem1  8898  epfrs  9172  dfac5lem4  9551  kmlem11  9585  ackbij1lem2  9642  fin23lem26  9746  isfin1-3  9807  hsmexlem4  9850  axdc3lem4  9874  axresscn  10569  nn0ssre  11900  nn0sscn  11901  xrsupss  12701  supxrmnf  12709  1exp  13457  hashxrcl  13717  hashdifsn  13774  hashdifsnp1  13853  repsdf2  14139  modfsummods  15147  fsum00  15152  incexc  15191  2ebits  15795  bitsinvp1  15797  lcmfunsnlem2lem1  15981  lcmfunsnlem2lem2  15982  lcmfunsnlem2  15983  coprmproddvdslem  16005  4sqlem19  16298  ramxrcl  16352  mrcsncl  16882  acsfn1  16931  homaf  17289  dmcoass  17325  lubel  17731  gsumws1  18001  cycsubg2  18352  cntzsnval  18453  0frgp  18904  dpjidcl  19179  ablfac1eu  19194  lspsncl  19748  lspsnss  19761  lspsnid  19764  lpival  20017  lpiss  20022  lidldvgen  20027  znlidl  20679  frlmlbs  20940  mat1dimelbas  21079  smadiadetglem2  21280  isneip  21712  neips  21720  opnneip  21726  maxlp  21754  restsn2  21778  leordtval2  21819  ist1-3  21956  ordtt1  21986  2ndcdisj2  22064  uffix  22528  neiflim  22581  ptcmplem5  22663  cnextfres1  22675  haustsms2  22744  ust0  22827  ustuqtop5  22853  dscopn  23182  icccmplem1  23429  bndth  23561  ovolsn  24095  icombl1  24163  plyun0  24786  coeeulem  24813  coeeu  24814  vieta1lem2  24899  aalioulem2  24921  taylfval  24946  perfectlem2  25805  istrkg2ld  26245  axlowdimlem7  26733  axlowdimlem10  26736  0clwlkv  27909  hsn0elch  29024  chsupsn  29189  chsup0  29324  h1deoi  29325  h1dei  29326  h1did  29327  h1de2ctlem  29331  h1de2ci  29332  spansni  29333  spansnch  29336  elspansncl  29341  spansnpji  29354  spanunsni  29355  spanpr  29356  h1datomi  29357  spansnji  29422  h1da  30125  atom1d  30129  superpos  30130  disjun0  30344  mptprop  30433  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  34282  lindsadd  34884  lindsenlbs  34886  poimirlem16  34907  poimirlem19  34910  poimirlem23  34914  poimirlem25  34916  poimirlem29  34920  poimirlem31  34922  mblfinlem2  34929  dvasin  34977  fdc  35019  prnc  35344  isfldidl  35345  ispridlc  35347  islshpsm  36115  snatpsubN  36885  polatN  37066  atpsubclN  37080  pclfinclN  37085  mapfzcons  39311  mzpcompact2lem  39346  diophrw  39354  brfvidRP  40031  cotrcltrcl  40068  corcltrcl  40082  cotrclrcl  40085  gneispa  40478  binomcxplemnotnn0  40686  snelpwrVD  41163  disjiun2  41318  infxrpnf  41719  mccllem  41876  islptre  41898  cncfdmsn  42171  snmbl  42246  stoweidlem44  42328  sge0tsms  42661  sge0iunmptlemfi  42694  ismeannd  42748  isomenndlem  42811  hoidmvlelem3  42878  hoidmvlelem4  42879  ovnhoilem1  42882  fnbrafvb  43352  afvres  43370  afv2res  43437  perfectALTVlem2  43886  mapsnop  44392  lincext2  44509  snlindsntorlem  44524  aacllem  44901