Theorem snssi 4744

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

Syntax hints:   → wi 4   ∈ wcel 2142   ⊆ wss 3904  {csn 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-ss 3921  df-sn 4583

This theorem is referenced by:  snssd  4745  difsnid  4768  eldifeldifsn  4769  pwpw0  4771  sssn  4784  ssunsn2  4785  tpssi  4796  frirr  5623  xpsspw  5782  djussxp  5817  dmressnsn  6009  fconst6g  6753  f1sng  6850  dffv2  6962  fvimacnvi  7033  fvimacnvALT  7038  fsn2  7118  fsnunf  7169  abnexg  7739  ordsuci  7791  curry1  8083  curry2  8086  xpord2pred  8125  xpord3pred  8132  ressuppss  8163  ressuppssdif  8165  naddcllem  8646  naddov2  8649  mapsnd  8868  ralxpmap  8878  fodomr  9100  findcard2  9133  findcard2s  9134  unfi  9139  ssfi  9141  sucdom2  9171  0sdom1dom  9190  enp1ilem  9222  fodomfir  9272  marypha1lem  9379  marypha2lem1  9381  epfrs  9686  dfac5lem4  10082  dfac5lem4OLD  10084  kmlem11  10117  ackbij1lem2  10176  fin23lem26  10282  isfin1-3  10343  hsmexlem4  10386  axdc3lem4  10410  axresscn  11106  nn0ssre  12485  nn0sscn  12486  xrsupss  13312  supxrmnf  13320  1exp  14104  hashxrcl  14370  hashdifsn  14427  hashdifsnp1  14519  repsdf2  14791  modfsummods  15821  fsum00  15826  incexc  15867  2ebits  16481  bitsinvp1  16483  lcmfunsnlem2lem1  16672  lcmfunsnlem2lem2  16673  lcmfunsnlem2  16674  coprmproddvdslem  16696  4sqlem19  16999  ramxrcl  17053  mrcsncl  17644  acsfn1  17693  homaf  18063  dmcoass  18099  lubel  18546  gsumws1  18872  eqg0subgecsn  19238  cycsubg2  19251  cntzsnval  19364  0frgp  19819  dpjidcl  20100  ablfac1eu  20115  lspsncl  21044  lspsnss  21057  lspsnid  21060  lpival  21394  lpiss  21399  lidldvgen  21404  pzriprnglem10  21542  znlidl  21585  frlmlbs  21849  mat1dimelbas  22531  smadiadetglem2  22732  isneip  23165  neips  23173  opnneip  23179  maxlp  23207  restsn2  23231  leordtval2  23272  ist1-3  23409  ordtt1  23439  2ndcdisj2  23517  uffix  23981  neiflim  24034  ptcmplem5  24116  cnextfres1  24128  haustsms2  24197  ust0  24280  ustuqtop5  24305  dscopn  24633  icccmplem1  24883  bndth  25020  ovolsn  25557  icombl1  25625  plyun0  26257  coeeulem  26284  coeeu  26285  vieta1lem2  26375  aalioulem2  26397  taylfval  26422  perfectlem2  27294  noextend  27730  noextendseq  27731  conway  27872  etaslts  27886  0lt1s  27905  sltsleft  27953  sltsright  27954  negsid  28134  precsexlem8  28307  precsexlem11  28310  n0bday  28445  elreno2  28588  istrkg2ld  28629  axlowdimlem7  29149  axlowdimlem10  29152  0clwlkv  30333  hsn0elch  31451  chsupsn  31616  chsup0  31751  h1deoi  31752  h1dei  31753  h1did  31754  h1de2ctlem  31758  h1de2ci  31759  spansni  31760  spansnch  31763  elspansncl  31768  spansnpji  31781  spanunsni  31782  spanpr  31783  h1datomi  31784  spansnji  31849  h1da  32552  atom1d  32556  superpos  32557  disjun0  32795  djussxp2  32850  mptprop  32900  pwrssmgc  33178  gsumwrd2dccatlem  33257  elrgspnsubrunlem2  33429  1fldgenq  33509  rspsnid  33557  lindssn  33564  elrspunidl  33614  esplyfval1  33870  esplyfvaln  33871  lbslsat  33913  fldextrspunlsplem  33970  esumnul  34345  esumcst  34360  hashf2  34381  esum2d  34390  measvuni  34511  cntnevol  34525  eulerpartlemt  34668  eulerpartlemmf  34672  eulerpartlemgh  34675  ballotlemfp1  34789  reprinfz1  34916  fineqvac  35412  f1resfz0f1d  35464  dfon2lem3  36133  altxpsspw  36327  ttcmin  36856  ttcsnmin  36878  bj-snglss  37455  lindsadd  38112  lindsenlbs  38114  poimirlem16  38135  poimirlem19  38138  poimirlem23  38142  poimirlem25  38144  poimirlem29  38148  poimirlem31  38150  mblfinlem2  38157  dvasin  38203  fdc  38244  prnc  38566  isfldidl  38567  ispridlc  38569  islshpsm  39604  snatpsubN  40374  polatN  40555  atpsubclN  40569  pclfinclN  40574  readvrec2  42970  mapfzcons  43297  mzpcompact2lem  43332  diophrw  43340  brfvidRP  44264  cotrcltrcl  44301  corcltrcl  44315  cotrclrcl  44318  gneispa  44706  binomcxplemnotnn0  44932  snelpwrVD  45406  disjiun2  45638  infxrpnf  46020  mccllem  46173  islptre  46195  cncfdmsn  46464  snmbl  46537  stoweidlem44  46618  sge0tsms  46954  sge0iunmptlemfi  46987  ismeannd  47041  isomenndlem  47104  hoidmvlelem3  47171  hoidmvlelem4  47172  ovnhoilem1  47175  fnbrafvb  47748  afvres  47766  afv2res  47833  perfectALTVlem2  48344  mapsnop  48966  lincext2  49077  snlindsntorlem  49092  resinsnALT  49494  aacllem  50422