Theorem snssi 4775

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3917  {csn 4592

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3934  df-sn 4593

This theorem is referenced by:  snssd  4776  difsnid  4777  eldifeldifsn  4778  pwpw0  4780  sssn  4793  ssunsn2  4794  tpssi  4805  snelpwiOLD  5407  intidOLD  5421  frirr  5617  xpsspw  5775  djussxp  5812  dmressnsn  5997  fconst6g  6752  f1sng  6845  dffv2  6959  fvimacnvi  7027  fvimacnvALT  7032  fsn2  7111  fsnunf  7162  abnexg  7735  ordsuci  7787  sucexeloniOLD  7789  curry1  8086  curry2  8089  xpord2pred  8127  xpord3pred  8134  ressuppss  8165  ressuppssdif  8167  naddcllem  8643  naddov2  8646  mapsnd  8862  ralxpmap  8872  sucdom2OLD  9056  fodomr  9098  findcard2  9134  findcard2s  9135  unfi  9141  ssfi  9143  sucdom2  9173  0sdom1dom  9192  en1eqsnOLD  9227  enp1ilem  9230  fodomfir  9286  marypha1lem  9391  marypha2lem1  9393  epfrs  9691  dfac5lem4  10086  dfac5lem4OLD  10088  kmlem11  10121  ackbij1lem2  10180  fin23lem26  10285  isfin1-3  10346  hsmexlem4  10389  axdc3lem4  10413  axresscn  11108  nn0ssre  12453  nn0sscn  12454  xrsupss  13276  supxrmnf  13284  1exp  14063  hashxrcl  14329  hashdifsn  14386  hashdifsnp1  14478  repsdf2  14750  modfsummods  15766  fsum00  15771  incexc  15810  2ebits  16424  bitsinvp1  16426  lcmfunsnlem2lem1  16615  lcmfunsnlem2lem2  16616  lcmfunsnlem2  16617  coprmproddvdslem  16639  4sqlem19  16941  ramxrcl  16995  mrcsncl  17580  acsfn1  17629  homaf  17999  dmcoass  18035  lubel  18480  gsumws1  18772  eqg0subgecsn  19136  cycsubg2  19149  cntzsnval  19263  0frgp  19716  dpjidcl  19997  ablfac1eu  20012  lspsncl  20890  lspsnss  20903  lspsnid  20906  lpival  21241  lpiss  21246  lidldvgen  21251  pzriprnglem10  21407  znlidl  21450  frlmlbs  21713  mat1dimelbas  22365  smadiadetglem2  22566  isneip  22999  neips  23007  opnneip  23013  maxlp  23041  restsn2  23065  leordtval2  23106  ist1-3  23243  ordtt1  23273  2ndcdisj2  23351  uffix  23815  neiflim  23868  ptcmplem5  23950  cnextfres1  23962  haustsms2  24031  ust0  24114  ustuqtop5  24140  dscopn  24468  icccmplem1  24718  bndth  24864  ovolsn  25403  icombl1  25471  plyun0  26109  coeeulem  26136  coeeu  26137  vieta1lem2  26226  aalioulem2  26248  taylfval  26273  perfectlem2  27148  noextend  27585  noextendseq  27586  conway  27718  etasslt  27732  0slt1s  27748  ssltleft  27789  ssltright  27790  negsid  27954  precsexlem8  28123  precsexlem11  28126  n0sbday  28251  istrkg2ld  28394  axlowdimlem7  28882  axlowdimlem10  28885  0clwlkv  30067  hsn0elch  31184  chsupsn  31349  chsup0  31484  h1deoi  31485  h1dei  31486  h1did  31487  h1de2ctlem  31491  h1de2ci  31492  spansni  31493  spansnch  31496  elspansncl  31501  spansnpji  31514  spanunsni  31515  spanpr  31516  h1datomi  31517  spansnji  31582  h1da  32285  atom1d  32289  superpos  32290  disjun0  32531  djussxp2  32579  mptprop  32628  pwrssmgc  32933  gsumwrd2dccatlem  33013  elrgspnsubrunlem2  33206  1fldgenq  33279  rspsnid  33349  lindssn  33356  elrspunidl  33406  lbslsat  33619  fldextrspunlsplem  33675  esumnul  34045  esumcst  34060  hashf2  34081  esum2d  34090  measvuni  34211  cntnevol  34225  eulerpartlemt  34369  eulerpartlemmf  34373  eulerpartlemgh  34376  ballotlemfp1  34490  reprinfz1  34620  fineqvac  35094  f1resfz0f1d  35108  dfon2lem3  35780  altxpsspw  35972  bj-snglss  36965  lindsadd  37614  lindsenlbs  37616  poimirlem16  37637  poimirlem19  37640  poimirlem23  37644  poimirlem25  37646  poimirlem29  37650  poimirlem31  37652  mblfinlem2  37659  dvasin  37705  fdc  37746  prnc  38068  isfldidl  38069  ispridlc  38071  islshpsm  38980  snatpsubN  39751  polatN  39932  atpsubclN  39946  pclfinclN  39951  readvrec2  42356  mapfzcons  42711  mzpcompact2lem  42746  diophrw  42754  brfvidRP  43684  cotrcltrcl  43721  corcltrcl  43735  cotrclrcl  43738  gneispa  44126  binomcxplemnotnn0  44352  snelpwrVD  44827  disjiun2  45059  infxrpnf  45449  mccllem  45602  islptre  45624  cncfdmsn  45895  snmbl  45968  stoweidlem44  46049  sge0tsms  46385  sge0iunmptlemfi  46418  ismeannd  46472  isomenndlem  46535  hoidmvlelem3  46602  hoidmvlelem4  46603  ovnhoilem1  46606  fnbrafvb  47159  afvres  47177  afv2res  47244  perfectALTVlem2  47727  mapsnop  48336  lincext2  48448  snlindsntorlem  48463  resinsnALT  48865  aacllem  49794