Theorem snssi 4742

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

Syntax hints:   → wi 4   ∈ wcel 2107   ⊆ wss 3888  {csn 4562

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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905  df-sn 4563

This theorem is referenced by:  snssd  4743  difsnid  4744  eldifeldifsn  4745  pwpw0  4747  sssn  4760  ssunsn2  4761  tpssi  4770  pwsnOLD  4833  snelpwi  5361  intid  5374  frirr  5567  xpsspw  5721  djussxp  5757  dmressnsn  5936  fconst6g  6672  f1sng  6767  dffv2  6872  fvimacnvi  6938  fvimacnvALT  6943  fsn2  7017  fsnunf  7066  abnexg  7615  sucexeloni  7667  suceloniOLD  7669  curry1  7953  curry2  7956  ressuppss  8008  ressuppssdif  8010  mapsnd  8683  ralxpmap  8693  sucdom2OLD  8878  fodomr  8924  findcard2  8956  findcard2s  8957  unfi  8964  ssfi  8965  sucdom2  8998  en1eqsn  9057  enp1ilem  9060  findcard2OLD  9065  marypha1lem  9201  marypha2lem1  9203  epfrs  9498  dfac5lem4  9891  kmlem11  9925  ackbij1lem2  9986  fin23lem26  10090  isfin1-3  10151  hsmexlem4  10194  axdc3lem4  10218  axresscn  10913  nn0ssre  12246  nn0sscn  12247  xrsupss  13052  supxrmnf  13060  1exp  13821  hashxrcl  14081  hashdifsn  14138  hashdifsnp1  14219  repsdf2  14500  modfsummods  15514  fsum00  15519  incexc  15558  2ebits  16163  bitsinvp1  16165  lcmfunsnlem2lem1  16352  lcmfunsnlem2lem2  16353  lcmfunsnlem2  16354  coprmproddvdslem  16376  4sqlem19  16673  ramxrcl  16727  mrcsncl  17330  acsfn1  17379  homaf  17754  dmcoass  17790  lubel  18241  gsumws1  18485  cycsubg2  18838  cntzsnval  18939  0frgp  19394  dpjidcl  19670  ablfac1eu  19685  lspsncl  20248  lspsnss  20261  lspsnid  20264  lpival  20525  lpiss  20530  lidldvgen  20535  znlidl  20746  frlmlbs  21013  mat1dimelbas  21629  smadiadetglem2  21830  isneip  22265  neips  22273  opnneip  22279  maxlp  22307  restsn2  22331  leordtval2  22372  ist1-3  22509  ordtt1  22539  2ndcdisj2  22617  uffix  23081  neiflim  23134  ptcmplem5  23216  cnextfres1  23228  haustsms2  23297  ust0  23380  ustuqtop5  23406  dscopn  23738  icccmplem1  23994  bndth  24130  ovolsn  24668  icombl1  24736  plyun0  25367  coeeulem  25394  coeeu  25395  vieta1lem2  25480  aalioulem2  25502  taylfval  25527  perfectlem2  26387  istrkg2ld  26830  axlowdimlem7  27325  axlowdimlem10  27328  0clwlkv  28504  hsn0elch  29619  chsupsn  29784  chsup0  29919  h1deoi  29920  h1dei  29921  h1did  29922  h1de2ctlem  29926  h1de2ci  29927  spansni  29928  spansnch  29931  elspansncl  29936  spansnpji  29949  spanunsni  29950  spanpr  29951  h1datomi  29952  spansnji  30017  h1da  30720  atom1d  30724  superpos  30725  disjun0  30943  djussxp2  30994  mptprop  31040  pwrssmgc  31287  rspsnid  31577  lindssn  31582  elrspunidl  31615  lbslsat  31708  esumnul  32025  esumcst  32040  hashf2  32061  esum2d  32070  measvuni  32191  cntnevol  32205  eulerpartlemt  32347  eulerpartlemmf  32351  eulerpartlemgh  32354  ballotlemfp1  32467  reprinfz1  32611  fineqvac  33075  f1resfz0f1d  33081  dfon2lem3  33770  xpord2pred  33801  xpord3pred  33807  naddcllem  33840  naddov2  33843  noextend  33878  noextendseq  33879  conway  34002  etasslt  34016  0slt1s  34032  ssltleft  34063  ssltright  34064  addscllem1  34140  altxpsspw  34288  bj-snglss  35169  lindsadd  35779  lindsenlbs  35781  poimirlem16  35802  poimirlem19  35805  poimirlem23  35809  poimirlem25  35811  poimirlem29  35815  poimirlem31  35817  mblfinlem2  35824  dvasin  35870  fdc  35912  prnc  36234  isfldidl  36235  ispridlc  36237  islshpsm  37001  snatpsubN  37771  polatN  37952  atpsubclN  37966  pclfinclN  37971  mapfzcons  40545  mzpcompact2lem  40580  diophrw  40588  brfvidRP  41303  cotrcltrcl  41340  corcltrcl  41354  cotrclrcl  41357  gneispa  41747  binomcxplemnotnn0  41981  snelpwrVD  42458  disjiun2  42613  infxrpnf  42993  mccllem  43145  islptre  43167  cncfdmsn  43438  snmbl  43511  stoweidlem44  43592  sge0tsms  43925  sge0iunmptlemfi  43958  ismeannd  44012  isomenndlem  44075  hoidmvlelem3  44142  hoidmvlelem4  44143  ovnhoilem1  44146  fnbrafvb  44657  afvres  44675  afv2res  44742  perfectALTVlem2  45185  mapsnop  45691  lincext2  45807  snlindsntorlem  45822  aacllem  46516