Theorem snssi 4746

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ⊆ wss 3899  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-ss 3916  df-sn 4585

This theorem is used by:  snssd  4747  difsnid  4771  eldifeldifsn  4772  pwpw0  4774  sssn  4787  ssunsn2  4788  tpssi  4798  frirr  5627  xpsspw  5787  djussxp  5823  dmressnsn  6012  fconst6g  6771  f1sng  6868  dffv2  6980  fvimacnvi  7051  fvimacnvALT  7056  fsn2  7137  fsnunf  7190  abnexg  7770  ordsuci  7822  curry1  8115  curry2  8118  xpord2pred  8162  xpord3pred  8169  ressuppss  8200  ressuppssdif  8202  naddcllem  8685  naddov2  8688  mapsnd  8914  ralxpmap  8924  fodomr  9147  findcard2  9180  findcard2s  9181  unfi  9186  ssfi  9188  sucdom2  9218  0sdom1dom  9237  enp1ilem  9269  fodomfir  9319  marypha1lem  9425  marypha2lem1  9427  epfrs  9732  hfsn  9920  dfac5lem4  10205  kmlem11  10239  ackbij1lem2  10298  fin23lem26  10403  isfin1-3  10464  hsmexlem4  10507  axdc3lem4  10531  axresscn  11233  nn0ssre  12610  nn0sscn  12611  xrsupss  13439  supxrmnf  13447  f1resfz0f1d  13927  1exp  14234  hashxrcl  14501  hashdifsn  14559  hashdifsnp1  14651  repsdf2  14929  modfsummods  15960  fsum00  15965  incexc  16006  2ebits  16617  bitsinvp1  16619  lcmfunsnlem2lem1  16813  lcmfunsnlem2lem2  16814  lcmfunsnlem2  16815  coprmproddvdslem  16837  4sqlem19  17141  ramxrcl  17195  mrcsncl  17786  acsfn1  17835  homaf  18205  dmcoass  18241  lubel  18688  gsumws1  19034  eqg0subgecsn  19412  cycsubg2  19425  cntzsnval  19538  0frgp  19993  dpjidcl  20274  ablfac1eu  20289  lspsncl  21252  lspsnss  21265  lspsnid  21268  rspsnid  21527  lpival  21648  lpiss  21653  lidldvgen  21658  pzriprnglem10  21796  znlidl  21839  frlmlbs  22103  lindsenlbs  22157  mat1dimelbas  22786  smadiadetglem2  22987  isneip  23423  neips  23431  opnneip  23437  maxlp  23465  restsn2  23489  leordtval2  23530  ist1-3  23667  ordtt1  23697  2ndcdisj2  23776  uffix  24240  neiflim  24293  ptcmplem5  24375  cnextfres1  24387  haustsms2  24456  ust0  24539  ustuqtop5  24564  dscopn  24892  icccmplem1  25142  bndth  25279  ovolsn  25816  icombl1  25884  plyun0  26515  coeeulem  26543  coeeu  26544  vieta1lem2  26634  aalioulem2  26660  taylfval  26686  perfectlem2  27557  noextend  28023  noextendseq  28024  conway  28165  etaslts  28179  0lt1s  28198  sltsleft  28246  sltsright  28247  negsid  28427  precsexlem8  28600  precsexlem11  28603  n0bday  28738  elreno2  28881  istrkg2ld  28922  axlowdimlem7  29526  axlowdimlem10  29529  0clwlkv  30722  hsn0elch  31850  chsupsn  32015  chsup0  32150  h1deoi  32151  h1dei  32152  h1did  32153  h1de2ctlem  32157  h1de2ci  32158  spansni  32159  spansnch  32162  elspansncl  32167  spansnpji  32180  spanunsni  32181  spanpr  32182  h1datomi  32183  spansnji  32248  h1da  32951  atom1d  32955  superpos  32956  disjun0  33189  djussxp2  33242  mptprop  33291  pwrssmgc  33561  gsumwrd2dccatlem  33638  elrgspnsubrunlem2  33809  1fldgenq  33884  lindssn  33933  elrspunidl  33978  esplyfval1  34205  esplyfvaln  34206  lbslsat  34248  fldextrspunlsplem  34305  esumnul  34680  esumcst  34695  hashf2  34716  esum2d  34725  measvuni  34847  cntnevol  34861  eulerpartlemt  35003  eulerpartlemmf  35007  eulerpartlemgh  35010  ballotlemfp1  35124  reprinfz1  35251  fineqvac  35784  dfon2lem3  36547  altxpsspw  36742  ttcmin  37284  ttcsnmin  37306  bj-snglss  37883  lindsadd  38536  poimirlem16  38554  poimirlem19  38557  poimirlem23  38561  poimirlem25  38563  poimirlem29  38567  poimirlem31  38569  mblfinlem2  38576  dvasin  38622  negprop  38643  fdc  38679  prnc  39001  isfldidl  39002  ispridlc  39004  islshpsm  40037  snatpsubN  40807  polatN  40988  atpsubclN  41002  pclfinclN  41007  readvrec2  43412  mapfzcons  43726  mzpcompact2lem  43761  diophrw  43769  brfvidRP  44687  cotrcltrcl  44724  corcltrcl  44738  cotrclrcl  44741  gneispa  45129  binomcxplemnotnn0  45339  snelpwrVD  45812  disjiun2  46074  infxrpnf  46455  mccllem  46608  islptre  46630  cncfdmsn  46899  snmbl  46972  stoweidlem44  47053  sge0tsms  47389  sge0iunmptlemfi  47422  ismeannd  47476  isomenndlem  47539  hoidmvlelem3  47606  hoidmvlelem4  47607  ovnhoilem1  47610  fnbrafvb  48223  afvres  48241  afv2res  48308  perfectALTVlem2  48819  mapsnop  49455  lincext2  49566  snlindsntorlem  49581  resinsnALT  49980  aacllem  50938