Theorem snssi 4752

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3890  {csn 4568

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-sn 4569

This theorem is referenced by:  snssd  4753  difsnid  4754  eldifeldifsn  4755  pwpw0  4757  sssn  4770  ssunsn2  4771  tpssi  4782  frirr  5601  xpsspw  5759  djussxp  5795  dmressnsn  5983  fconst6g  6724  f1sng  6818  dffv2  6930  fvimacnvi  6999  fvimacnvALT  7004  fsn2  7084  fsnunf  7134  abnexg  7704  ordsuci  7756  curry1  8048  curry2  8051  xpord2pred  8089  xpord3pred  8096  ressuppss  8127  ressuppssdif  8129  naddcllem  8606  naddov2  8609  mapsnd  8828  ralxpmap  8838  fodomr  9060  findcard2  9093  findcard2s  9094  unfi  9099  ssfi  9101  sucdom2  9131  0sdom1dom  9150  enp1ilem  9182  fodomfir  9232  marypha1lem  9340  marypha2lem1  9342  epfrs  9646  dfac5lem4  10042  dfac5lem4OLD  10044  kmlem11  10077  ackbij1lem2  10136  fin23lem26  10241  isfin1-3  10302  hsmexlem4  10345  axdc3lem4  10369  axresscn  11065  nn0ssre  12435  nn0sscn  12436  xrsupss  13255  supxrmnf  13263  1exp  14047  hashxrcl  14313  hashdifsn  14370  hashdifsnp1  14462  repsdf2  14734  modfsummods  15750  fsum00  15755  incexc  15796  2ebits  16410  bitsinvp1  16412  lcmfunsnlem2lem1  16601  lcmfunsnlem2lem2  16602  lcmfunsnlem2  16603  coprmproddvdslem  16625  4sqlem19  16928  ramxrcl  16982  mrcsncl  17572  acsfn1  17621  homaf  17991  dmcoass  18027  lubel  18474  gsumws1  18800  eqg0subgecsn  19166  cycsubg2  19179  cntzsnval  19293  0frgp  19748  dpjidcl  20029  ablfac1eu  20044  lspsncl  20966  lspsnss  20979  lspsnid  20982  lpival  21317  lpiss  21322  lidldvgen  21327  pzriprnglem10  21483  znlidl  21526  frlmlbs  21790  mat1dimelbas  22449  smadiadetglem2  22650  isneip  23083  neips  23091  opnneip  23097  maxlp  23125  restsn2  23149  leordtval2  23190  ist1-3  23327  ordtt1  23357  2ndcdisj2  23435  uffix  23899  neiflim  23952  ptcmplem5  24034  cnextfres1  24046  haustsms2  24115  ust0  24198  ustuqtop5  24223  dscopn  24551  icccmplem1  24801  bndth  24938  ovolsn  25475  icombl1  25543  plyun0  26175  coeeulem  26202  coeeu  26203  vieta1lem2  26291  aalioulem2  26313  taylfval  26338  perfectlem2  27210  noextend  27647  noextendseq  27648  conway  27788  etaslts  27802  0lt1s  27821  sltsleft  27869  sltsright  27870  negsid  28050  precsexlem8  28223  precsexlem11  28226  n0bday  28361  elreno2  28504  istrkg2ld  28545  axlowdimlem7  29034  axlowdimlem10  29037  0clwlkv  30219  hsn0elch  31337  chsupsn  31502  chsup0  31637  h1deoi  31638  h1dei  31639  h1did  31640  h1de2ctlem  31644  h1de2ci  31645  spansni  31646  spansnch  31649  elspansncl  31654  spansnpji  31667  spanunsni  31668  spanpr  31669  h1datomi  31670  spansnji  31735  h1da  32438  atom1d  32442  superpos  32443  disjun0  32683  djussxp2  32739  mptprop  32789  pwrssmgc  33078  gsumwrd2dccatlem  33156  elrgspnsubrunlem2  33327  1fldgenq  33401  rspsnid  33449  lindssn  33456  elrspunidl  33506  esplyfval1  33735  esplyfvaln  33736  lbslsat  33779  fldextrspunlsplem  33836  esumnul  34211  esumcst  34226  hashf2  34247  esum2d  34256  measvuni  34377  cntnevol  34391  eulerpartlemt  34534  eulerpartlemmf  34538  eulerpartlemgh  34541  ballotlemfp1  34655  reprinfz1  34785  fineqvac  35279  f1resfz0f1d  35315  dfon2lem3  35984  altxpsspw  36178  ttcmin  36697  ttcsnmin  36719  bj-snglss  37296  lindsadd  37951  lindsenlbs  37953  poimirlem16  37974  poimirlem19  37977  poimirlem23  37981  poimirlem25  37983  poimirlem29  37987  poimirlem31  37989  mblfinlem2  37996  dvasin  38042  fdc  38083  prnc  38405  isfldidl  38406  ispridlc  38408  islshpsm  39443  snatpsubN  40213  polatN  40394  atpsubclN  40408  pclfinclN  40413  readvrec2  42810  mapfzcons  43165  mzpcompact2lem  43200  diophrw  43208  brfvidRP  44136  cotrcltrcl  44173  corcltrcl  44187  cotrclrcl  44190  gneispa  44578  binomcxplemnotnn0  44804  snelpwrVD  45278  disjiun2  45510  infxrpnf  45895  mccllem  46048  islptre  46070  cncfdmsn  46339  snmbl  46412  stoweidlem44  46493  sge0tsms  46829  sge0iunmptlemfi  46862  ismeannd  46916  isomenndlem  46979  hoidmvlelem3  47046  hoidmvlelem4  47047  ovnhoilem1  47050  fnbrafvb  47617  afvres  47635  afv2res  47702  perfectALTVlem2  48213  mapsnop  48835  lincext2  48946  snlindsntorlem  48961  resinsnALT  49363  aacllem  50291