Theorem snssi 4762

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

Syntax hints:   → wi 4   ∈ wcel 2113   ⊆ wss 3899  {csn 4578

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 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-ss 3916  df-sn 4579

This theorem is referenced by:  snssd  4763  difsnid  4764  eldifeldifsn  4765  pwpw0  4767  sssn  4780  ssunsn2  4781  tpssi  4792  frirr  5598  xpsspw  5756  djussxp  5792  dmressnsn  5980  fconst6g  6721  f1sng  6815  dffv2  6927  fvimacnvi  6995  fvimacnvALT  7000  fsn2  7079  fsnunf  7129  abnexg  7699  ordsuci  7751  curry1  8044  curry2  8047  xpord2pred  8085  xpord3pred  8092  ressuppss  8123  ressuppssdif  8125  naddcllem  8602  naddov2  8605  mapsnd  8822  ralxpmap  8832  fodomr  9054  findcard2  9087  findcard2s  9088  unfi  9093  ssfi  9095  sucdom2  9125  0sdom1dom  9144  enp1ilem  9176  fodomfir  9226  marypha1lem  9334  marypha2lem1  9336  epfrs  9638  dfac5lem4  10034  dfac5lem4OLD  10036  kmlem11  10069  ackbij1lem2  10128  fin23lem26  10233  isfin1-3  10294  hsmexlem4  10337  axdc3lem4  10361  axresscn  11057  nn0ssre  12403  nn0sscn  12404  xrsupss  13222  supxrmnf  13230  1exp  14012  hashxrcl  14278  hashdifsn  14335  hashdifsnp1  14427  repsdf2  14699  modfsummods  15714  fsum00  15719  incexc  15758  2ebits  16372  bitsinvp1  16374  lcmfunsnlem2lem1  16563  lcmfunsnlem2lem2  16564  lcmfunsnlem2  16565  coprmproddvdslem  16587  4sqlem19  16889  ramxrcl  16943  mrcsncl  17533  acsfn1  17582  homaf  17952  dmcoass  17988  lubel  18435  gsumws1  18761  eqg0subgecsn  19124  cycsubg2  19137  cntzsnval  19251  0frgp  19706  dpjidcl  19987  ablfac1eu  20002  lspsncl  20926  lspsnss  20939  lspsnid  20942  lpival  21277  lpiss  21282  lidldvgen  21287  pzriprnglem10  21443  znlidl  21486  frlmlbs  21750  mat1dimelbas  22413  smadiadetglem2  22614  isneip  23047  neips  23055  opnneip  23061  maxlp  23089  restsn2  23113  leordtval2  23154  ist1-3  23291  ordtt1  23321  2ndcdisj2  23399  uffix  23863  neiflim  23916  ptcmplem5  23998  cnextfres1  24010  haustsms2  24079  ust0  24162  ustuqtop5  24187  dscopn  24515  icccmplem1  24765  bndth  24911  ovolsn  25450  icombl1  25518  plyun0  26156  coeeulem  26183  coeeu  26184  vieta1lem2  26273  aalioulem2  26295  taylfval  26320  perfectlem2  27195  noextend  27632  noextendseq  27633  conway  27767  etasslt  27781  0slt1s  27800  ssltleft  27842  ssltright  27843  negsid  28010  precsexlem8  28182  precsexlem11  28185  n0sbday  28312  elreno2  28440  istrkg2ld  28481  axlowdimlem7  28970  axlowdimlem10  28973  0clwlkv  30155  hsn0elch  31272  chsupsn  31437  chsup0  31572  h1deoi  31573  h1dei  31574  h1did  31575  h1de2ctlem  31579  h1de2ci  31580  spansni  31581  spansnch  31584  elspansncl  31589  spansnpji  31602  spanunsni  31603  spanpr  31604  h1datomi  31605  spansnji  31670  h1da  32373  atom1d  32377  superpos  32378  disjun0  32619  djussxp2  32675  mptprop  32726  pwrssmgc  33031  gsumwrd2dccatlem  33108  elrgspnsubrunlem2  33279  1fldgenq  33353  rspsnid  33401  lindssn  33408  elrspunidl  33458  lbslsat  33722  fldextrspunlsplem  33779  esumnul  34154  esumcst  34169  hashf2  34190  esum2d  34199  measvuni  34320  cntnevol  34334  eulerpartlemt  34477  eulerpartlemmf  34481  eulerpartlemgh  34484  ballotlemfp1  34598  reprinfz1  34728  fineqvac  35221  f1resfz0f1d  35257  dfon2lem3  35926  altxpsspw  36120  bj-snglss  37114  lindsadd  37753  lindsenlbs  37755  poimirlem16  37776  poimirlem19  37779  poimirlem23  37783  poimirlem25  37785  poimirlem29  37789  poimirlem31  37791  mblfinlem2  37798  dvasin  37844  fdc  37885  prnc  38207  isfldidl  38208  ispridlc  38210  islshpsm  39179  snatpsubN  39949  polatN  40130  atpsubclN  40144  pclfinclN  40149  readvrec2  42558  mapfzcons  42900  mzpcompact2lem  42935  diophrw  42943  brfvidRP  43871  cotrcltrcl  43908  corcltrcl  43922  cotrclrcl  43925  gneispa  44313  binomcxplemnotnn0  44539  snelpwrVD  45013  disjiun2  45245  infxrpnf  45632  mccllem  45785  islptre  45807  cncfdmsn  46076  snmbl  46149  stoweidlem44  46230  sge0tsms  46566  sge0iunmptlemfi  46599  ismeannd  46653  isomenndlem  46716  hoidmvlelem3  46783  hoidmvlelem4  46784  ovnhoilem1  46787  fnbrafvb  47342  afvres  47360  afv2res  47427  perfectALTVlem2  47910  mapsnop  48532  lincext2  48643  snlindsntorlem  48658  resinsnALT  49060  aacllem  49988