Theorem snssi 4751

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2143   ⊆ wss 3905  {csn 4589

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-ss 3922  df-sn 4590

This theorem is used by:  snssd  4752  difsnid  4776  eldifeldifsn  4777  pwpw0  4779  sssn  4792  ssunsn2  4793  tpssi  4803  frirr  5637  xpsspw  5796  djussxp  5831  dmressnsn  6022  fconst6g  6767  f1sng  6864  dffv2  6976  fvimacnvi  7047  fvimacnvALT  7052  fsn2  7132  fsnunf  7183  abnexg  7751  ordsuci  7803  curry1  8095  curry2  8098  xpord2pred  8137  xpord3pred  8144  ressuppss  8175  ressuppssdif  8177  naddcllem  8658  naddov2  8661  mapsnd  8880  ralxpmap  8890  fodomr  9112  findcard2  9145  findcard2s  9146  unfi  9151  ssfi  9153  sucdom2  9183  0sdom1dom  9202  enp1ilem  9234  fodomfir  9283  marypha1lem  9389  marypha2lem1  9391  epfrs  9696  dfac5lem4  10115  kmlem11  10149  ackbij1lem2  10208  fin23lem26  10313  isfin1-3  10374  hsmexlem4  10417  axdc3lem4  10441  axresscn  11137  nn0ssre  12512  nn0sscn  12513  xrsupss  13339  supxrmnf  13347  1exp  14132  hashxrcl  14398  hashdifsn  14456  hashdifsnp1  14548  repsdf2  14820  modfsummods  15850  fsum00  15855  incexc  15896  2ebits  16509  bitsinvp1  16511  lcmfunsnlem2lem1  16700  lcmfunsnlem2lem2  16701  lcmfunsnlem2  16702  coprmproddvdslem  16724  4sqlem19  17027  ramxrcl  17081  mrcsncl  17672  acsfn1  17721  homaf  18091  dmcoass  18127  lubel  18574  gsumws1  18901  eqg0subgecsn  19272  cycsubg2  19285  cntzsnval  19398  0frgp  19853  dpjidcl  20134  ablfac1eu  20149  lspsncl  21107  lspsnss  21120  lspsnid  21123  rspsnid  21382  lpival  21501  lpiss  21506  lidldvgen  21511  pzriprnglem10  21649  znlidl  21692  frlmlbs  21956  mat1dimelbas  22637  smadiadetglem2  22838  isneip  23271  neips  23279  opnneip  23285  maxlp  23313  restsn2  23337  leordtval2  23378  ist1-3  23515  ordtt1  23545  2ndcdisj2  23623  uffix  24087  neiflim  24140  ptcmplem5  24222  cnextfres1  24234  haustsms2  24303  ust0  24386  ustuqtop5  24411  dscopn  24739  icccmplem1  24989  bndth  25126  ovolsn  25663  icombl1  25731  plyun0  26363  coeeulem  26390  coeeu  26391  vieta1lem2  26481  aalioulem2  26505  taylfval  26531  perfectlem2  27403  noextend  27839  noextendseq  27840  conway  27981  etaslts  27995  0lt1s  28014  sltsleft  28062  sltsright  28063  negsid  28243  precsexlem8  28416  precsexlem11  28419  n0bday  28554  elreno2  28697  istrkg2ld  28738  axlowdimlem7  29307  axlowdimlem10  29310  0clwlkv  30491  hsn0elch  31609  chsupsn  31774  chsup0  31909  h1deoi  31910  h1dei  31911  h1did  31912  h1de2ctlem  31916  h1de2ci  31917  spansni  31918  spansnch  31921  elspansncl  31926  spansnpji  31939  spanunsni  31940  spanpr  31941  h1datomi  31942  spansnji  32007  h1da  32710  atom1d  32714  superpos  32715  disjun0  32949  djussxp2  33002  mptprop  33052  pwrssmgc  33329  gsumwrd2dccatlem  33406  elrgspnsubrunlem2  33577  1fldgenq  33652  lindssn  33700  elrspunidl  33745  esplyfval1  33972  esplyfvaln  33973  lbslsat  34015  fldextrspunlsplem  34072  esumnul  34447  esumcst  34462  hashf2  34483  esum2d  34492  measvuni  34613  cntnevol  34627  eulerpartlemt  34770  eulerpartlemmf  34774  eulerpartlemgh  34777  ballotlemfp1  34891  reprinfz1  35018  fineqvac  35537  f1resfz0f1d  35613  dfon2lem3  36283  altxpsspw  36477  ttcmin  37035  ttcsnmin  37057  bj-snglss  37634  lindsadd  38292  lindsenlbs  38294  poimirlem16  38315  poimirlem19  38318  poimirlem23  38322  poimirlem25  38324  poimirlem29  38328  poimirlem31  38330  mblfinlem2  38337  dvasin  38383  fdc  38424  prnc  38746  isfldidl  38747  ispridlc  38749  islshpsm  39782  snatpsubN  40552  polatN  40733  atpsubclN  40747  pclfinclN  40752  readvrec2  43150  mapfzcons  43475  mzpcompact2lem  43510  diophrw  43518  brfvidRP  44442  cotrcltrcl  44479  corcltrcl  44493  cotrclrcl  44496  gneispa  44884  binomcxplemnotnn0  45094  snelpwrVD  45567  disjiun2  45806  infxrpnf  46188  mccllem  46341  islptre  46363  cncfdmsn  46632  snmbl  46705  stoweidlem44  46786  sge0tsms  47122  sge0iunmptlemfi  47155  ismeannd  47209  isomenndlem  47272  hoidmvlelem3  47339  hoidmvlelem4  47340  ovnhoilem1  47343  fnbrafvb  47919  afvres  47937  afv2res  48004  perfectALTVlem2  48515  mapsnop  49152  lincext2  49263  snlindsntorlem  49278  resinsnALT  49679  aacllem  50649