Theorem snssi 4759

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3903  {csn 4577

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 3438  df-ss 3920  df-sn 4578

This theorem is referenced by:  snssd  4760  difsnid  4761  eldifeldifsn  4762  pwpw0  4764  sssn  4777  ssunsn2  4778  tpssi  4789  snelpwiOLD  5387  intidOLD  5401  frirr  5595  xpsspw  5752  djussxp  5788  dmressnsn  5974  fconst6g  6713  f1sng  6806  dffv2  6918  fvimacnvi  6986  fvimacnvALT  6991  fsn2  7070  fsnunf  7121  abnexg  7692  ordsuci  7744  curry1  8037  curry2  8040  xpord2pred  8078  xpord3pred  8085  ressuppss  8116  ressuppssdif  8118  naddcllem  8594  naddov2  8597  mapsnd  8813  ralxpmap  8823  fodomr  9045  findcard2  9078  findcard2s  9079  unfi  9085  ssfi  9087  sucdom2  9117  0sdom1dom  9135  enp1ilem  9167  fodomfir  9218  marypha1lem  9323  marypha2lem1  9325  epfrs  9627  dfac5lem4  10020  dfac5lem4OLD  10022  kmlem11  10055  ackbij1lem2  10114  fin23lem26  10219  isfin1-3  10280  hsmexlem4  10323  axdc3lem4  10347  axresscn  11042  nn0ssre  12388  nn0sscn  12389  xrsupss  13211  supxrmnf  13219  1exp  13998  hashxrcl  14264  hashdifsn  14321  hashdifsnp1  14413  repsdf2  14684  modfsummods  15700  fsum00  15705  incexc  15744  2ebits  16358  bitsinvp1  16360  lcmfunsnlem2lem1  16549  lcmfunsnlem2lem2  16550  lcmfunsnlem2  16551  coprmproddvdslem  16573  4sqlem19  16875  ramxrcl  16929  mrcsncl  17518  acsfn1  17567  homaf  17937  dmcoass  17973  lubel  18420  gsumws1  18712  eqg0subgecsn  19076  cycsubg2  19089  cntzsnval  19203  0frgp  19658  dpjidcl  19939  ablfac1eu  19954  lspsncl  20880  lspsnss  20893  lspsnid  20896  lpival  21231  lpiss  21236  lidldvgen  21241  pzriprnglem10  21397  znlidl  21440  frlmlbs  21704  mat1dimelbas  22356  smadiadetglem2  22557  isneip  22990  neips  22998  opnneip  23004  maxlp  23032  restsn2  23056  leordtval2  23097  ist1-3  23234  ordtt1  23264  2ndcdisj2  23342  uffix  23806  neiflim  23859  ptcmplem5  23941  cnextfres1  23953  haustsms2  24022  ust0  24105  ustuqtop5  24131  dscopn  24459  icccmplem1  24709  bndth  24855  ovolsn  25394  icombl1  25462  plyun0  26100  coeeulem  26127  coeeu  26128  vieta1lem2  26217  aalioulem2  26239  taylfval  26264  perfectlem2  27139  noextend  27576  noextendseq  27577  conway  27710  etasslt  27724  0slt1s  27743  ssltleft  27784  ssltright  27785  negsid  27952  precsexlem8  28121  precsexlem11  28124  n0sbday  28249  istrkg2ld  28405  axlowdimlem7  28893  axlowdimlem10  28896  0clwlkv  30075  hsn0elch  31192  chsupsn  31357  chsup0  31492  h1deoi  31493  h1dei  31494  h1did  31495  h1de2ctlem  31499  h1de2ci  31500  spansni  31501  spansnch  31504  elspansncl  31509  spansnpji  31522  spanunsni  31523  spanpr  31524  h1datomi  31525  spansnji  31590  h1da  32293  atom1d  32297  superpos  32298  disjun0  32539  djussxp2  32592  mptprop  32641  pwrssmgc  32943  gsumwrd2dccatlem  33020  elrgspnsubrunlem2  33189  1fldgenq  33262  rspsnid  33309  lindssn  33316  elrspunidl  33366  lbslsat  33589  fldextrspunlsplem  33646  esumnul  34021  esumcst  34036  hashf2  34057  esum2d  34066  measvuni  34187  cntnevol  34201  eulerpartlemt  34345  eulerpartlemmf  34349  eulerpartlemgh  34352  ballotlemfp1  34466  reprinfz1  34596  fineqvac  35078  f1resfz0f1d  35097  dfon2lem3  35769  altxpsspw  35961  bj-snglss  36954  lindsadd  37603  lindsenlbs  37605  poimirlem16  37626  poimirlem19  37629  poimirlem23  37633  poimirlem25  37635  poimirlem29  37639  poimirlem31  37641  mblfinlem2  37648  dvasin  37694  fdc  37735  prnc  38057  isfldidl  38058  ispridlc  38060  islshpsm  38969  snatpsubN  39739  polatN  39920  atpsubclN  39934  pclfinclN  39939  readvrec2  42344  mapfzcons  42699  mzpcompact2lem  42734  diophrw  42742  brfvidRP  43671  cotrcltrcl  43708  corcltrcl  43722  cotrclrcl  43725  gneispa  44113  binomcxplemnotnn0  44339  snelpwrVD  44814  disjiun2  45046  infxrpnf  45435  mccllem  45588  islptre  45610  cncfdmsn  45881  snmbl  45954  stoweidlem44  46035  sge0tsms  46371  sge0iunmptlemfi  46404  ismeannd  46458  isomenndlem  46521  hoidmvlelem3  46588  hoidmvlelem4  46589  ovnhoilem1  46592  fnbrafvb  47148  afvres  47166  afv2res  47233  perfectALTVlem2  47716  mapsnop  48338  lincext2  48450  snlindsntorlem  48465  resinsnALT  48867  aacllem  49796