Theorem snssi 4784

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

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3926  {csn 4601

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-ss 3943  df-sn 4602

This theorem is referenced by:  snssd  4785  difsnid  4786  eldifeldifsn  4787  pwpw0  4789  sssn  4802  ssunsn2  4803  tpssi  4814  snelpwiOLD  5419  intidOLD  5433  frirr  5630  xpsspw  5788  djussxp  5825  dmressnsn  6010  fconst6g  6767  f1sng  6860  dffv2  6974  fvimacnvi  7042  fvimacnvALT  7047  fsn2  7126  fsnunf  7177  abnexg  7750  ordsuci  7802  sucexeloniOLD  7804  suceloniOLD  7806  curry1  8103  curry2  8106  xpord2pred  8144  xpord3pred  8151  ressuppss  8182  ressuppssdif  8184  naddcllem  8688  naddov2  8691  mapsnd  8900  ralxpmap  8910  sucdom2OLD  9096  fodomr  9142  findcard2  9178  findcard2s  9179  unfi  9185  ssfi  9187  sucdom2  9217  0sdom1dom  9246  en1eqsnOLD  9281  enp1ilem  9284  fodomfir  9340  marypha1lem  9445  marypha2lem1  9447  epfrs  9745  dfac5lem4  10140  dfac5lem4OLD  10142  kmlem11  10175  ackbij1lem2  10234  fin23lem26  10339  isfin1-3  10400  hsmexlem4  10443  axdc3lem4  10467  axresscn  11162  nn0ssre  12505  nn0sscn  12506  xrsupss  13325  supxrmnf  13333  1exp  14109  hashxrcl  14375  hashdifsn  14432  hashdifsnp1  14524  repsdf2  14796  modfsummods  15809  fsum00  15814  incexc  15853  2ebits  16466  bitsinvp1  16468  lcmfunsnlem2lem1  16657  lcmfunsnlem2lem2  16658  lcmfunsnlem2  16659  coprmproddvdslem  16681  4sqlem19  16983  ramxrcl  17037  mrcsncl  17624  acsfn1  17673  homaf  18043  dmcoass  18079  lubel  18524  gsumws1  18816  eqg0subgecsn  19180  cycsubg2  19193  cntzsnval  19307  0frgp  19760  dpjidcl  20041  ablfac1eu  20056  lspsncl  20934  lspsnss  20947  lspsnid  20950  lpival  21285  lpiss  21290  lidldvgen  21295  pzriprnglem10  21451  znlidl  21494  frlmlbs  21757  mat1dimelbas  22409  smadiadetglem2  22610  isneip  23043  neips  23051  opnneip  23057  maxlp  23085  restsn2  23109  leordtval2  23150  ist1-3  23287  ordtt1  23317  2ndcdisj2  23395  uffix  23859  neiflim  23912  ptcmplem5  23994  cnextfres1  24006  haustsms2  24075  ust0  24158  ustuqtop5  24184  dscopn  24512  icccmplem1  24762  bndth  24908  ovolsn  25448  icombl1  25516  plyun0  26154  coeeulem  26181  coeeu  26182  vieta1lem2  26271  aalioulem2  26293  taylfval  26318  perfectlem2  27193  noextend  27630  noextendseq  27631  conway  27763  etasslt  27777  0slt1s  27793  ssltleft  27834  ssltright  27835  negsid  27999  precsexlem8  28168  precsexlem11  28171  n0sbday  28296  istrkg2ld  28439  axlowdimlem7  28927  axlowdimlem10  28930  0clwlkv  30112  hsn0elch  31229  chsupsn  31394  chsup0  31529  h1deoi  31530  h1dei  31531  h1did  31532  h1de2ctlem  31536  h1de2ci  31537  spansni  31538  spansnch  31541  elspansncl  31546  spansnpji  31559  spanunsni  31560  spanpr  31561  h1datomi  31562  spansnji  31627  h1da  32330  atom1d  32334  superpos  32335  disjun0  32576  djussxp2  32626  mptprop  32675  pwrssmgc  32980  gsumwrd2dccatlem  33060  elrgspnsubrunlem2  33243  1fldgenq  33316  rspsnid  33386  lindssn  33393  elrspunidl  33443  lbslsat  33656  fldextrspunlsplem  33714  esumnul  34079  esumcst  34094  hashf2  34115  esum2d  34124  measvuni  34245  cntnevol  34259  eulerpartlemt  34403  eulerpartlemmf  34407  eulerpartlemgh  34410  ballotlemfp1  34524  reprinfz1  34654  fineqvac  35128  f1resfz0f1d  35136  dfon2lem3  35803  altxpsspw  35995  bj-snglss  36988  lindsadd  37637  lindsenlbs  37639  poimirlem16  37660  poimirlem19  37663  poimirlem23  37667  poimirlem25  37669  poimirlem29  37673  poimirlem31  37675  mblfinlem2  37682  dvasin  37728  fdc  37769  prnc  38091  isfldidl  38092  ispridlc  38094  islshpsm  38998  snatpsubN  39769  polatN  39950  atpsubclN  39964  pclfinclN  39969  readvrec2  42404  mapfzcons  42739  mzpcompact2lem  42774  diophrw  42782  brfvidRP  43712  cotrcltrcl  43749  corcltrcl  43763  cotrclrcl  43766  gneispa  44154  binomcxplemnotnn0  44380  snelpwrVD  44855  disjiun2  45082  infxrpnf  45473  mccllem  45626  islptre  45648  cncfdmsn  45919  snmbl  45992  stoweidlem44  46073  sge0tsms  46409  sge0iunmptlemfi  46442  ismeannd  46496  isomenndlem  46559  hoidmvlelem3  46626  hoidmvlelem4  46627  ovnhoilem1  46630  fnbrafvb  47183  afvres  47201  afv2res  47268  perfectALTVlem2  47736  mapsnop  48319  lincext2  48431  snlindsntorlem  48446  resinsnALT  48848  aacllem  49665