Theorem snssi 4748

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   ⊆ wss 3900  {csn 4588

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-sn 4589

This theorem is used by:  snssd  4749  difsnid  4773  eldifeldifsn  4774  sssn  4787  ssunsn2  4788  tpssi  4798  pwpw0  4836  frirr  5634  xpsspw  5796  djussxp  5833  dmressnsn  6030  fconst6g  6801  f1sng  6899  dffv2  7011  fvimacnvi  7082  fvimacnvALT  7087  fsn2  7169  fsnunf  7221  abnexg  7802  ordsuci  7856  curry1  8152  curry2  8155  xpord2pred  8199  xpord3pred  8206  ressuppss  8238  ressuppssdif  8240  naddcllem  8723  naddov2  8726  mapsnd  8952  ralxpmap  8962  fodomr  9185  findcard2  9218  findcard2s  9219  unfi  9224  ssfi  9226  sucdom2  9256  0sdom1dom  9275  enp1ilem  9307  fodomfir  9357  marypha1lem  9462  marypha2lem1  9464  epfrs  9769  hfsn  9957  dfac5lem4  10244  kmlem11  10278  ackbij1lem2  10337  fin23lem26  10442  isfin1-3  10503  hsmexlem4  10546  axdc3lem4  10570  axresscn  11272  nn0ssre  12650  nn0sscn  12651  xrsupss  13479  supxrmnf  13487  f1resfz0f1d  13967  1exp  14274  hashxrcl  14542  hashdifsn  14600  hashdifsnp1  14692  repsdf2  14971  modfsummods  16004  fsum00  16009  incexc  16050  2ebits  16661  bitsinvp1  16663  lcmfunsnlem2lem1  16857  lcmfunsnlem2lem2  16858  lcmfunsnlem2  16859  coprmproddvdslem  16881  4sqlem19  17185  ramxrcl  17239  mrcsncl  17836  acsfn1  17885  homaf  18255  dmcoass  18291  lubel  18738  gsumws1  19084  eqg0subgecsn  19462  cycsubg2  19475  cntzsnval  19589  0frgp  20044  dpjidcl  20325  ablfac1eu  20340  lspsncl  21303  lspsnss  21316  lspsnid  21319  rspsnid  21578  lpival  21699  lpiss  21704  lidldvgen  21709  pzriprnglem10  21851  znlidl  21894  frlmlbs  22158  lindsenlbs  22212  mat1dimelbas  22841  smadiadetglem2  23042  isneip  23478  neips  23486  opnneip  23492  maxlp  23520  restsn2  23544  leordtval2  23585  ist1-3  23722  ordtt1  23752  2ndcdisj2  23831  uffix  24295  neiflim  24348  ptcmplem5  24430  cnextfres1  24442  haustsms2  24511  ust0  24594  ustuqtop5  24619  dscopn  24947  icccmplem1  25197  bndth  25334  ovolsn  25871  icombl1  25939  plyun0  26570  coeeulem  26598  coeeu  26599  vieta1lem2  26689  aalioulem2  26717  taylfval  26743  perfectlem2  27614  noextend  28080  noextendseq  28081  conway  28222  etaslts  28236  0lt1s  28255  sltsleft  28303  sltsright  28304  negsid  28484  precsexlem8  28657  precsexlem11  28660  n0bday  28795  elreno2  28938  istrkg2ld  28979  axlowdimlem7  29583  axlowdimlem10  29586  0clwlkv  30779  hsn0elch  31907  chsupsn  32072  chsup0  32207  h1deoi  32208  h1dei  32209  h1did  32210  h1de2ctlem  32214  h1de2ci  32215  spansni  32216  spansnch  32219  elspansncl  32224  spansnpji  32237  spanunsni  32238  spanpr  32239  h1datomi  32240  spansnji  32305  h1da  33008  atom1d  33012  superpos  33013  disjun0  33287  djussxp2  33340  mptprop  33388  pwrssmgc  33660  gsumwrd2dccatlem  33737  elrgspnsubrunlem2  33908  1fldgenq  33988  lindssn  34037  elrspunidl  34082  esplyfval1  34316  esplyfvaln  34317  lbslsat  34359  fldextrspunlsplem  34416  esumnul  34791  esumcst  34806  hashf2  34827  esum2d  34836  measvuni  34958  cntnevol  34972  eulerpartlemt  35114  eulerpartlemmf  35118  eulerpartlemgh  35121  ballotlemfp1  35235  reprinfz1  35362  fineqvac  35925  elpssmo  36673  dfon2lem3  36762  altxpsspw  36957  ttcmin  37499  ttcsnmin  37521  bj-snglss  38098  lindsadd  38804  poimirlem16  38822  poimirlem19  38825  poimirlem23  38829  poimirlem25  38831  poimirlem29  38835  poimirlem31  38837  mblfinlem2  38844  dvasin  38890  negprop  38911  fdc  38945  prnc  39267  isfldidl  39268  ispridlc  39270  islshpsm  40303  snatpsubN  41073  polatN  41254  atpsubclN  41268  pclfinclN  41273  readvrec2  43678  mapfzcons  43993  mzpcompact2lem  44028  diophrw  44036  brfvidRP  44949  cotrcltrcl  44986  corcltrcl  45000  cotrclrcl  45003  gneispa  45391  binomcxplemnotnn0  45601  snelpwrVD  46073  disjiun2  46349  infxrpnf  46729  mccllem  46882  islptre  46904  cncfdmsn  47173  snmbl  47246  stoweidlem44  47327  sge0tsms  47663  sge0iunmptlemfi  47696  ismeannd  47750  isomenndlem  47813  hoidmvlelem3  47880  hoidmvlelem4  47881  ovnhoilem1  47884  fnbrafvb  48497  afvres  48515  afv2res  48582  perfectALTVlem2  49093  azssid  49718  azcn  49720  mapsnop  49787  lincext2  49898  snlindsntorlem  49913  resinsnALT  50317  aacllem  51367