Theorem snssi 4772

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3914  {csn 4589

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-ss 3931  df-sn 4590

This theorem is referenced by:  snssd  4773  difsnid  4774  eldifeldifsn  4775  pwpw0  4777  sssn  4790  ssunsn2  4791  tpssi  4802  snelpwiOLD  5404  intidOLD  5418  frirr  5614  xpsspw  5772  djussxp  5809  dmressnsn  5994  fconst6g  6749  f1sng  6842  dffv2  6956  fvimacnvi  7024  fvimacnvALT  7029  fsn2  7108  fsnunf  7159  abnexg  7732  ordsuci  7784  sucexeloniOLD  7786  curry1  8083  curry2  8086  xpord2pred  8124  xpord3pred  8131  ressuppss  8162  ressuppssdif  8164  naddcllem  8640  naddov2  8643  mapsnd  8859  ralxpmap  8869  fodomr  9092  findcard2  9128  findcard2s  9129  unfi  9135  ssfi  9137  sucdom2  9167  0sdom1dom  9185  en1eqsnOLD  9220  enp1ilem  9223  fodomfir  9279  marypha1lem  9384  marypha2lem1  9386  epfrs  9684  dfac5lem4  10079  dfac5lem4OLD  10081  kmlem11  10114  ackbij1lem2  10173  fin23lem26  10278  isfin1-3  10339  hsmexlem4  10382  axdc3lem4  10406  axresscn  11101  nn0ssre  12446  nn0sscn  12447  xrsupss  13269  supxrmnf  13277  1exp  14056  hashxrcl  14322  hashdifsn  14379  hashdifsnp1  14471  repsdf2  14743  modfsummods  15759  fsum00  15764  incexc  15803  2ebits  16417  bitsinvp1  16419  lcmfunsnlem2lem1  16608  lcmfunsnlem2lem2  16609  lcmfunsnlem2  16610  coprmproddvdslem  16632  4sqlem19  16934  ramxrcl  16988  mrcsncl  17573  acsfn1  17622  homaf  17992  dmcoass  18028  lubel  18473  gsumws1  18765  eqg0subgecsn  19129  cycsubg2  19142  cntzsnval  19256  0frgp  19709  dpjidcl  19990  ablfac1eu  20005  lspsncl  20883  lspsnss  20896  lspsnid  20899  lpival  21234  lpiss  21239  lidldvgen  21244  pzriprnglem10  21400  znlidl  21443  frlmlbs  21706  mat1dimelbas  22358  smadiadetglem2  22559  isneip  22992  neips  23000  opnneip  23006  maxlp  23034  restsn2  23058  leordtval2  23099  ist1-3  23236  ordtt1  23266  2ndcdisj2  23344  uffix  23808  neiflim  23861  ptcmplem5  23943  cnextfres1  23955  haustsms2  24024  ust0  24107  ustuqtop5  24133  dscopn  24461  icccmplem1  24711  bndth  24857  ovolsn  25396  icombl1  25464  plyun0  26102  coeeulem  26129  coeeu  26130  vieta1lem2  26219  aalioulem2  26241  taylfval  26266  perfectlem2  27141  noextend  27578  noextendseq  27579  conway  27711  etasslt  27725  0slt1s  27741  ssltleft  27782  ssltright  27783  negsid  27947  precsexlem8  28116  precsexlem11  28119  n0sbday  28244  istrkg2ld  28387  axlowdimlem7  28875  axlowdimlem10  28878  0clwlkv  30060  hsn0elch  31177  chsupsn  31342  chsup0  31477  h1deoi  31478  h1dei  31479  h1did  31480  h1de2ctlem  31484  h1de2ci  31485  spansni  31486  spansnch  31489  elspansncl  31494  spansnpji  31507  spanunsni  31508  spanpr  31509  h1datomi  31510  spansnji  31575  h1da  32278  atom1d  32282  superpos  32283  disjun0  32524  djussxp2  32572  mptprop  32621  pwrssmgc  32926  gsumwrd2dccatlem  33006  elrgspnsubrunlem2  33199  1fldgenq  33272  rspsnid  33342  lindssn  33349  elrspunidl  33399  lbslsat  33612  fldextrspunlsplem  33668  esumnul  34038  esumcst  34053  hashf2  34074  esum2d  34083  measvuni  34204  cntnevol  34218  eulerpartlemt  34362  eulerpartlemmf  34366  eulerpartlemgh  34369  ballotlemfp1  34483  reprinfz1  34613  fineqvac  35087  f1resfz0f1d  35101  dfon2lem3  35773  altxpsspw  35965  bj-snglss  36958  lindsadd  37607  lindsenlbs  37609  poimirlem16  37630  poimirlem19  37633  poimirlem23  37637  poimirlem25  37639  poimirlem29  37643  poimirlem31  37645  mblfinlem2  37652  dvasin  37698  fdc  37739  prnc  38061  isfldidl  38062  ispridlc  38064  islshpsm  38973  snatpsubN  39744  polatN  39925  atpsubclN  39939  pclfinclN  39944  readvrec2  42349  mapfzcons  42704  mzpcompact2lem  42739  diophrw  42747  brfvidRP  43677  cotrcltrcl  43714  corcltrcl  43728  cotrclrcl  43731  gneispa  44119  binomcxplemnotnn0  44345  snelpwrVD  44820  disjiun2  45052  infxrpnf  45442  mccllem  45595  islptre  45617  cncfdmsn  45888  snmbl  45961  stoweidlem44  46042  sge0tsms  46378  sge0iunmptlemfi  46411  ismeannd  46465  isomenndlem  46528  hoidmvlelem3  46595  hoidmvlelem4  46596  ovnhoilem1  46599  fnbrafvb  47155  afvres  47173  afv2res  47240  perfectALTVlem2  47723  mapsnop  48332  lincext2  48444  snlindsntorlem  48459  resinsnALT  48861  aacllem  49790