Theorem snssi 4729

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-sn 4568

This theorem is referenced by:  snssd  4730  difsnid  4753  eldifeldifsn  4754  pwpw0  4756  sssn  4769  ssunsn2  4770  tpssi  4781  frirr  5607  xpsspw  5765  djussxp  5800  dmressnsn  5988  fconst6g  6729  f1sng  6823  dffv2  6935  fvimacnvi  7004  fvimacnvALT  7009  fsn2  7089  fsnunf  7140  abnexg  7710  ordsuci  7762  curry1  8054  curry2  8057  xpord2pred  8095  xpord3pred  8102  ressuppss  8133  ressuppssdif  8135  naddcllem  8612  naddov2  8615  mapsnd  8834  ralxpmap  8844  fodomr  9066  findcard2  9099  findcard2s  9100  unfi  9105  ssfi  9107  sucdom2  9137  0sdom1dom  9156  enp1ilem  9188  fodomfir  9238  marypha1lem  9346  marypha2lem1  9348  epfrs  9652  dfac5lem4  10048  dfac5lem4OLD  10050  kmlem11  10083  ackbij1lem2  10142  fin23lem26  10247  isfin1-3  10308  hsmexlem4  10351  axdc3lem4  10375  axresscn  11071  nn0ssre  12441  nn0sscn  12442  xrsupss  13261  supxrmnf  13269  1exp  14053  hashxrcl  14319  hashdifsn  14376  hashdifsnp1  14468  repsdf2  14740  modfsummods  15756  fsum00  15761  incexc  15802  2ebits  16416  bitsinvp1  16418  lcmfunsnlem2lem1  16607  lcmfunsnlem2lem2  16608  lcmfunsnlem2  16609  coprmproddvdslem  16631  4sqlem19  16934  ramxrcl  16988  mrcsncl  17578  acsfn1  17627  homaf  17997  dmcoass  18033  lubel  18480  gsumws1  18806  eqg0subgecsn  19172  cycsubg2  19185  cntzsnval  19299  0frgp  19754  dpjidcl  20035  ablfac1eu  20050  lspsncl  20972  lspsnss  20985  lspsnid  20988  lpival  21322  lpiss  21327  lidldvgen  21332  pzriprnglem10  21470  znlidl  21513  frlmlbs  21777  mat1dimelbas  22436  smadiadetglem2  22637  isneip  23070  neips  23078  opnneip  23084  maxlp  23112  restsn2  23136  leordtval2  23177  ist1-3  23314  ordtt1  23344  2ndcdisj2  23422  uffix  23886  neiflim  23939  ptcmplem5  24021  cnextfres1  24033  haustsms2  24102  ust0  24185  ustuqtop5  24210  dscopn  24538  icccmplem1  24788  bndth  24925  ovolsn  25462  icombl1  25530  plyun0  26162  coeeulem  26189  coeeu  26190  vieta1lem2  26277  aalioulem2  26299  taylfval  26324  perfectlem2  27193  noextend  27630  noextendseq  27631  conway  27771  etaslts  27785  0lt1s  27804  sltsleft  27852  sltsright  27853  negsid  28033  precsexlem8  28206  precsexlem11  28209  n0bday  28344  elreno2  28487  istrkg2ld  28528  axlowdimlem7  29017  axlowdimlem10  29020  0clwlkv  30201  hsn0elch  31319  chsupsn  31484  chsup0  31619  h1deoi  31620  h1dei  31621  h1did  31622  h1de2ctlem  31626  h1de2ci  31627  spansni  31628  spansnch  31631  elspansncl  31636  spansnpji  31649  spanunsni  31650  spanpr  31651  h1datomi  31652  spansnji  31717  h1da  32420  atom1d  32424  superpos  32425  disjun0  32665  djussxp2  32721  mptprop  32771  pwrssmgc  33060  gsumwrd2dccatlem  33138  elrgspnsubrunlem2  33309  1fldgenq  33383  rspsnid  33431  lindssn  33438  elrspunidl  33488  esplyfval1  33717  esplyfvaln  33718  lbslsat  33760  fldextrspunlsplem  33817  esumnul  34192  esumcst  34207  hashf2  34228  esum2d  34237  measvuni  34358  cntnevol  34372  eulerpartlemt  34515  eulerpartlemmf  34519  eulerpartlemgh  34522  ballotlemfp1  34636  reprinfz1  34766  fineqvac  35260  f1resfz0f1d  35296  dfon2lem3  35965  altxpsspw  36159  ttcmin  36678  ttcsnmin  36700  bj-snglss  37277  lindsadd  37934  lindsenlbs  37936  poimirlem16  37957  poimirlem19  37960  poimirlem23  37964  poimirlem25  37966  poimirlem29  37970  poimirlem31  37972  mblfinlem2  37979  dvasin  38025  fdc  38066  prnc  38388  isfldidl  38389  ispridlc  38391  islshpsm  39426  snatpsubN  40196  polatN  40377  atpsubclN  40391  pclfinclN  40396  readvrec2  42793  mapfzcons  43148  mzpcompact2lem  43183  diophrw  43191  brfvidRP  44115  cotrcltrcl  44152  corcltrcl  44166  cotrclrcl  44169  gneispa  44557  binomcxplemnotnn0  44783  snelpwrVD  45257  disjiun2  45489  infxrpnf  45874  mccllem  46027  islptre  46049  cncfdmsn  46318  snmbl  46391  stoweidlem44  46472  sge0tsms  46808  sge0iunmptlemfi  46841  ismeannd  46895  isomenndlem  46958  hoidmvlelem3  47025  hoidmvlelem4  47026  ovnhoilem1  47029  fnbrafvb  47602  afvres  47620  afv2res  47687  perfectALTVlem2  48198  mapsnop  48820  lincext2  48931  snlindsntorlem  48946  resinsnALT  49348  aacllem  50276