Theorem snssi 4812

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

Syntax hints:   → wi 4   ∈ wcel 2107   ⊆ wss 3949  {csn 4629

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-sn 4630

This theorem is referenced by:  snssd  4813  difsnid  4814  eldifeldifsn  4815  pwpw0  4817  sssn  4830  ssunsn2  4831  tpssi  4840  pwsnOLD  4902  snelpwiOLD  5445  intidOLD  5459  frirr  5654  xpsspw  5810  djussxp  5846  dmressnsn  6024  fconst6g  6781  f1sng  6876  dffv2  6987  fvimacnvi  7054  fvimacnvALT  7059  fsn2  7134  fsnunf  7183  abnexg  7743  ordsuci  7796  sucexeloniOLD  7798  suceloniOLD  7800  curry1  8090  curry2  8093  xpord2pred  8131  xpord3pred  8138  ressuppss  8168  ressuppssdif  8170  naddcllem  8675  naddov2  8678  mapsnd  8880  ralxpmap  8890  sucdom2OLD  9082  fodomr  9128  findcard2  9164  findcard2s  9165  unfi  9172  ssfi  9173  sucdom2  9206  0sdom1dom  9238  en1eqsnOLD  9275  enp1ilem  9278  findcard2OLD  9284  marypha1lem  9428  marypha2lem1  9430  epfrs  9726  dfac5lem4  10121  kmlem11  10155  ackbij1lem2  10216  fin23lem26  10320  isfin1-3  10381  hsmexlem4  10424  axdc3lem4  10448  axresscn  11143  nn0ssre  12476  nn0sscn  12477  xrsupss  13288  supxrmnf  13296  1exp  14057  hashxrcl  14317  hashdifsn  14374  hashdifsnp1  14457  repsdf2  14728  modfsummods  15739  fsum00  15744  incexc  15783  2ebits  16388  bitsinvp1  16390  lcmfunsnlem2lem1  16575  lcmfunsnlem2lem2  16576  lcmfunsnlem2  16577  coprmproddvdslem  16599  4sqlem19  16896  ramxrcl  16950  mrcsncl  17556  acsfn1  17605  homaf  17980  dmcoass  18016  lubel  18467  gsumws1  18719  eqg0subgecsn  19074  cycsubg2  19087  cntzsnval  19188  0frgp  19647  dpjidcl  19928  ablfac1eu  19943  lspsncl  20588  lspsnss  20601  lspsnid  20604  lpival  20883  lpiss  20888  lidldvgen  20893  znlidl  21085  frlmlbs  21352  mat1dimelbas  21973  smadiadetglem2  22174  isneip  22609  neips  22617  opnneip  22623  maxlp  22651  restsn2  22675  leordtval2  22716  ist1-3  22853  ordtt1  22883  2ndcdisj2  22961  uffix  23425  neiflim  23478  ptcmplem5  23560  cnextfres1  23572  haustsms2  23641  ust0  23724  ustuqtop5  23750  dscopn  24082  icccmplem1  24338  bndth  24474  ovolsn  25012  icombl1  25080  plyun0  25711  coeeulem  25738  coeeu  25739  vieta1lem2  25824  aalioulem2  25846  taylfval  25871  perfectlem2  26733  noextend  27169  noextendseq  27170  conway  27300  etasslt  27314  0slt1s  27330  ssltleft  27365  ssltright  27366  negsid  27515  precsexlem8  27660  precsexlem11  27663  istrkg2ld  27711  axlowdimlem7  28206  axlowdimlem10  28209  0clwlkv  29384  hsn0elch  30501  chsupsn  30666  chsup0  30801  h1deoi  30802  h1dei  30803  h1did  30804  h1de2ctlem  30808  h1de2ci  30809  spansni  30810  spansnch  30813  elspansncl  30818  spansnpji  30831  spanunsni  30832  spanpr  30833  h1datomi  30834  spansnji  30899  h1da  31602  atom1d  31606  superpos  31607  disjun0  31826  djussxp2  31873  mptprop  31920  pwrssmgc  32170  1fldgenq  32412  rspsnid  32485  lindssn  32494  elrspunidl  32546  lbslsat  32701  esumnul  33046  esumcst  33061  hashf2  33082  esum2d  33091  measvuni  33212  cntnevol  33226  eulerpartlemt  33370  eulerpartlemmf  33374  eulerpartlemgh  33377  ballotlemfp1  33490  reprinfz1  33634  fineqvac  34097  f1resfz0f1d  34103  dfon2lem3  34757  altxpsspw  34949  bj-snglss  35851  lindsadd  36481  lindsenlbs  36483  poimirlem16  36504  poimirlem19  36507  poimirlem23  36511  poimirlem25  36513  poimirlem29  36517  poimirlem31  36519  mblfinlem2  36526  dvasin  36572  fdc  36613  prnc  36935  isfldidl  36936  ispridlc  36938  islshpsm  37850  snatpsubN  38621  polatN  38802  atpsubclN  38816  pclfinclN  38821  mapfzcons  41454  mzpcompact2lem  41489  diophrw  41497  brfvidRP  42439  cotrcltrcl  42476  corcltrcl  42490  cotrclrcl  42493  gneispa  42881  binomcxplemnotnn0  43115  snelpwrVD  43592  disjiun2  43745  infxrpnf  44156  mccllem  44313  islptre  44335  cncfdmsn  44606  snmbl  44679  stoweidlem44  44760  sge0tsms  45096  sge0iunmptlemfi  45129  ismeannd  45183  isomenndlem  45246  hoidmvlelem3  45313  hoidmvlelem4  45314  ovnhoilem1  45317  fnbrafvb  45862  afvres  45880  afv2res  45947  perfectALTVlem2  46390  pzriprnglem10  46814  mapsnop  47020  lincext2  47136  snlindsntorlem  47151  aacllem  47848