Theorem snssi 4812

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

Syntax hints:   → wi 4   ∈ wcel 2107   ⊆ wss 3949  {csn 4629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-sn 4630

This theorem is referenced by:  snssd  4813  difsnid  4814  eldifeldifsn  4815  pwpw0  4817  sssn  4830  ssunsn2  4831  tpssi  4840  pwsnOLD  4902  snelpwiOLD  5445  intidOLD  5459  frirr  5654  xpsspw  5810  djussxp  5846  dmressnsn  6024  fconst6g  6781  f1sng  6876  dffv2  6987  fvimacnvi  7054  fvimacnvALT  7059  fsn2  7134  fsnunf  7183  abnexg  7743  ordsuci  7796  sucexeloniOLD  7798  suceloniOLD  7800  curry1  8090  curry2  8093  xpord2pred  8131  xpord3pred  8138  ressuppss  8168  ressuppssdif  8170  naddcllem  8675  naddov2  8678  mapsnd  8880  ralxpmap  8890  sucdom2OLD  9082  fodomr  9128  findcard2  9164  findcard2s  9165  unfi  9172  ssfi  9173  sucdom2  9206  0sdom1dom  9238  en1eqsnOLD  9275  enp1ilem  9278  findcard2OLD  9284  marypha1lem  9428  marypha2lem1  9430  epfrs  9726  dfac5lem4  10121  kmlem11  10155  ackbij1lem2  10216  fin23lem26  10320  isfin1-3  10381  hsmexlem4  10424  axdc3lem4  10448  axresscn  11143  nn0ssre  12476  nn0sscn  12477  xrsupss  13288  supxrmnf  13296  1exp  14057  hashxrcl  14317  hashdifsn  14374  hashdifsnp1  14457  repsdf2  14728  modfsummods  15739  fsum00  15744  incexc  15783  2ebits  16388  bitsinvp1  16390  lcmfunsnlem2lem1  16575  lcmfunsnlem2lem2  16576  lcmfunsnlem2  16577  coprmproddvdslem  16599  4sqlem19  16896  ramxrcl  16950  mrcsncl  17556  acsfn1  17605  homaf  17980  dmcoass  18016  lubel  18467  gsumws1  18719  eqg0subgecsn  19074  cycsubg2  19087  cntzsnval  19188  0frgp  19647  dpjidcl  19928  ablfac1eu  19943  lspsncl  20588  lspsnss  20601  lspsnid  20604  lpival  20883  lpiss  20888  lidldvgen  20893  znlidl  21085  frlmlbs  21352  mat1dimelbas  21973  smadiadetglem2  22174  isneip  22609  neips  22617  opnneip  22623  maxlp  22651  restsn2  22675  leordtval2  22716  ist1-3  22853  ordtt1  22883  2ndcdisj2  22961  uffix  23425  neiflim  23478  ptcmplem5  23560  cnextfres1  23572  haustsms2  23641  ust0  23724  ustuqtop5  23750  dscopn  24082  icccmplem1  24338  bndth  24474  ovolsn  25012  icombl1  25080  plyun0  25711  coeeulem  25738  coeeu  25739  vieta1lem2  25824  aalioulem2  25846  taylfval  25871  perfectlem2  26733  noextend  27169  noextendseq  27170  conway  27301  etasslt  27315  0slt1s  27331  ssltleft  27366  ssltright  27367  negsid  27518  precsexlem8  27663  precsexlem11  27666  istrkg2ld  27742  axlowdimlem7  28237  axlowdimlem10  28240  0clwlkv  29415  hsn0elch  30532  chsupsn  30697  chsup0  30832  h1deoi  30833  h1dei  30834  h1did  30835  h1de2ctlem  30839  h1de2ci  30840  spansni  30841  spansnch  30844  elspansncl  30849  spansnpji  30862  spanunsni  30863  spanpr  30864  h1datomi  30865  spansnji  30930  h1da  31633  atom1d  31637  superpos  31638  disjun0  31857  djussxp2  31904  mptprop  31951  pwrssmgc  32201  1fldgenq  32443  rspsnid  32516  lindssn  32525  elrspunidl  32577  lbslsat  32732  esumnul  33077  esumcst  33092  hashf2  33113  esum2d  33122  measvuni  33243  cntnevol  33257  eulerpartlemt  33401  eulerpartlemmf  33405  eulerpartlemgh  33408  ballotlemfp1  33521  reprinfz1  33665  fineqvac  34128  f1resfz0f1d  34134  dfon2lem3  34788  altxpsspw  34980  bj-snglss  35899  lindsadd  36529  lindsenlbs  36531  poimirlem16  36552  poimirlem19  36555  poimirlem23  36559  poimirlem25  36561  poimirlem29  36565  poimirlem31  36567  mblfinlem2  36574  dvasin  36620  fdc  36661  prnc  36983  isfldidl  36984  ispridlc  36986  islshpsm  37898  snatpsubN  38669  polatN  38850  atpsubclN  38864  pclfinclN  38869  mapfzcons  41502  mzpcompact2lem  41537  diophrw  41545  brfvidRP  42487  cotrcltrcl  42524  corcltrcl  42538  cotrclrcl  42541  gneispa  42929  binomcxplemnotnn0  43163  snelpwrVD  43640  disjiun2  43793  infxrpnf  44204  mccllem  44361  islptre  44383  cncfdmsn  44654  snmbl  44727  stoweidlem44  44808  sge0tsms  45144  sge0iunmptlemfi  45177  ismeannd  45231  isomenndlem  45294  hoidmvlelem3  45361  hoidmvlelem4  45362  ovnhoilem1  45365  fnbrafvb  45910  afvres  45928  afv2res  45995  perfectALTVlem2  46438  pzriprnglem10  46862  mapsnop  47068  lincext2  47184  snlindsntorlem  47199  aacllem  47896