Theorem snssi 4764

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

Syntax hints:   → wi 4   ∈ wcel 2113   ⊆ wss 3901  {csn 4580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-ss 3918  df-sn 4581

This theorem is referenced by:  snssd  4765  difsnid  4766  eldifeldifsn  4767  pwpw0  4769  sssn  4782  ssunsn2  4783  tpssi  4794  frirr  5600  xpsspw  5758  djussxp  5794  dmressnsn  5982  fconst6g  6723  f1sng  6817  dffv2  6929  fvimacnvi  6997  fvimacnvALT  7002  fsn2  7081  fsnunf  7131  abnexg  7701  ordsuci  7753  curry1  8046  curry2  8049  xpord2pred  8087  xpord3pred  8094  ressuppss  8125  ressuppssdif  8127  naddcllem  8604  naddov2  8607  mapsnd  8824  ralxpmap  8834  fodomr  9056  findcard2  9089  findcard2s  9090  unfi  9095  ssfi  9097  sucdom2  9127  0sdom1dom  9146  enp1ilem  9178  fodomfir  9228  marypha1lem  9336  marypha2lem1  9338  epfrs  9640  dfac5lem4  10036  dfac5lem4OLD  10038  kmlem11  10071  ackbij1lem2  10130  fin23lem26  10235  isfin1-3  10296  hsmexlem4  10339  axdc3lem4  10363  axresscn  11059  nn0ssre  12405  nn0sscn  12406  xrsupss  13224  supxrmnf  13232  1exp  14014  hashxrcl  14280  hashdifsn  14337  hashdifsnp1  14429  repsdf2  14701  modfsummods  15716  fsum00  15721  incexc  15760  2ebits  16374  bitsinvp1  16376  lcmfunsnlem2lem1  16565  lcmfunsnlem2lem2  16566  lcmfunsnlem2  16567  coprmproddvdslem  16589  4sqlem19  16891  ramxrcl  16945  mrcsncl  17535  acsfn1  17584  homaf  17954  dmcoass  17990  lubel  18437  gsumws1  18763  eqg0subgecsn  19126  cycsubg2  19139  cntzsnval  19253  0frgp  19708  dpjidcl  19989  ablfac1eu  20004  lspsncl  20928  lspsnss  20941  lspsnid  20944  lpival  21279  lpiss  21284  lidldvgen  21289  pzriprnglem10  21445  znlidl  21488  frlmlbs  21752  mat1dimelbas  22415  smadiadetglem2  22616  isneip  23049  neips  23057  opnneip  23063  maxlp  23091  restsn2  23115  leordtval2  23156  ist1-3  23293  ordtt1  23323  2ndcdisj2  23401  uffix  23865  neiflim  23918  ptcmplem5  24000  cnextfres1  24012  haustsms2  24081  ust0  24164  ustuqtop5  24189  dscopn  24517  icccmplem1  24767  bndth  24913  ovolsn  25452  icombl1  25520  plyun0  26158  coeeulem  26185  coeeu  26186  vieta1lem2  26275  aalioulem2  26297  taylfval  26322  perfectlem2  27197  noextend  27634  noextendseq  27635  conway  27775  etaslts  27789  0lt1s  27808  sltsleft  27856  sltsright  27857  negsid  28037  precsexlem8  28210  precsexlem11  28213  n0bday  28348  elreno2  28491  istrkg2ld  28532  axlowdimlem7  29021  axlowdimlem10  29024  0clwlkv  30206  hsn0elch  31323  chsupsn  31488  chsup0  31623  h1deoi  31624  h1dei  31625  h1did  31626  h1de2ctlem  31630  h1de2ci  31631  spansni  31632  spansnch  31635  elspansncl  31640  spansnpji  31653  spanunsni  31654  spanpr  31655  h1datomi  31656  spansnji  31721  h1da  32424  atom1d  32428  superpos  32429  disjun0  32670  djussxp2  32726  mptprop  32777  pwrssmgc  33082  gsumwrd2dccatlem  33159  elrgspnsubrunlem2  33330  1fldgenq  33404  rspsnid  33452  lindssn  33459  elrspunidl  33509  lbslsat  33773  fldextrspunlsplem  33830  esumnul  34205  esumcst  34220  hashf2  34241  esum2d  34250  measvuni  34371  cntnevol  34385  eulerpartlemt  34528  eulerpartlemmf  34532  eulerpartlemgh  34535  ballotlemfp1  34649  reprinfz1  34779  fineqvac  35272  f1resfz0f1d  35308  dfon2lem3  35977  altxpsspw  36171  bj-snglss  37171  lindsadd  37814  lindsenlbs  37816  poimirlem16  37837  poimirlem19  37840  poimirlem23  37844  poimirlem25  37846  poimirlem29  37850  poimirlem31  37852  mblfinlem2  37859  dvasin  37905  fdc  37946  prnc  38268  isfldidl  38269  ispridlc  38271  islshpsm  39250  snatpsubN  40020  polatN  40201  atpsubclN  40215  pclfinclN  40220  readvrec2  42626  mapfzcons  42968  mzpcompact2lem  43003  diophrw  43011  brfvidRP  43939  cotrcltrcl  43976  corcltrcl  43990  cotrclrcl  43993  gneispa  44381  binomcxplemnotnn0  44607  snelpwrVD  45081  disjiun2  45313  infxrpnf  45700  mccllem  45853  islptre  45875  cncfdmsn  46144  snmbl  46217  stoweidlem44  46298  sge0tsms  46634  sge0iunmptlemfi  46667  ismeannd  46721  isomenndlem  46784  hoidmvlelem3  46851  hoidmvlelem4  46852  ovnhoilem1  46855  fnbrafvb  47410  afvres  47428  afv2res  47495  perfectALTVlem2  47978  mapsnop  48600  lincext2  48711  snlindsntorlem  48726  resinsnALT  49128  aacllem  50056