Theorem snssi 4751

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

Syntax hints:   → wi 4   ∈ wcel 2143   ⊆ wss 3905  {csn 4589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-ss 3922  df-sn 4590

This theorem is referenced by:  snssd  4752  difsnid  4776  eldifeldifsn  4777  pwpw0  4779  sssn  4792  ssunsn2  4793  tpssi  4803  frirr  5637  xpsspw  5796  djussxp  5831  dmressnsn  6022  fconst6g  6767  f1sng  6864  dffv2  6976  fvimacnvi  7047  fvimacnvALT  7052  fsn2  7132  fsnunf  7183  abnexg  7751  ordsuci  7803  curry1  8095  curry2  8098  xpord2pred  8137  xpord3pred  8144  ressuppss  8175  ressuppssdif  8177  naddcllem  8658  naddov2  8661  mapsnd  8880  ralxpmap  8890  fodomr  9112  findcard2  9145  findcard2s  9146  unfi  9151  ssfi  9153  sucdom2  9183  0sdom1dom  9202  enp1ilem  9234  fodomfir  9283  marypha1lem  9389  marypha2lem1  9391  epfrs  9696  dfac5lem4  10106  kmlem11  10140  ackbij1lem2  10199  fin23lem26  10304  isfin1-3  10365  hsmexlem4  10408  axdc3lem4  10432  axresscn  11128  nn0ssre  12503  nn0sscn  12504  xrsupss  13330  supxrmnf  13338  1exp  14123  hashxrcl  14389  hashdifsn  14447  hashdifsnp1  14539  repsdf2  14811  modfsummods  15841  fsum00  15846  incexc  15887  2ebits  16500  bitsinvp1  16502  lcmfunsnlem2lem1  16691  lcmfunsnlem2lem2  16692  lcmfunsnlem2  16693  coprmproddvdslem  16715  4sqlem19  17018  ramxrcl  17072  mrcsncl  17663  acsfn1  17712  homaf  18082  dmcoass  18118  lubel  18565  gsumws1  18892  eqg0subgecsn  19263  cycsubg2  19276  cntzsnval  19389  0frgp  19844  dpjidcl  20125  ablfac1eu  20140  lspsncl  21098  lspsnss  21111  lspsnid  21114  rspsnid  21373  lpival  21492  lpiss  21497  lidldvgen  21502  pzriprnglem10  21640  znlidl  21683  frlmlbs  21947  mat1dimelbas  22628  smadiadetglem2  22829  isneip  23262  neips  23270  opnneip  23276  maxlp  23304  restsn2  23328  leordtval2  23369  ist1-3  23506  ordtt1  23536  2ndcdisj2  23614  uffix  24078  neiflim  24131  ptcmplem5  24213  cnextfres1  24225  haustsms2  24294  ust0  24377  ustuqtop5  24402  dscopn  24730  icccmplem1  24980  bndth  25117  ovolsn  25654  icombl1  25722  plyun0  26354  coeeulem  26381  coeeu  26382  vieta1lem2  26472  aalioulem2  26496  taylfval  26522  perfectlem2  27394  noextend  27830  noextendseq  27831  conway  27972  etaslts  27986  0lt1s  28005  sltsleft  28053  sltsright  28054  negsid  28234  precsexlem8  28407  precsexlem11  28410  n0bday  28545  elreno2  28688  istrkg2ld  28729  axlowdimlem7  29298  axlowdimlem10  29301  0clwlkv  30482  hsn0elch  31600  chsupsn  31765  chsup0  31900  h1deoi  31901  h1dei  31902  h1did  31903  h1de2ctlem  31907  h1de2ci  31908  spansni  31909  spansnch  31912  elspansncl  31917  spansnpji  31930  spanunsni  31931  spanpr  31932  h1datomi  31933  spansnji  31998  h1da  32701  atom1d  32705  superpos  32706  disjun0  32940  djussxp2  32993  mptprop  33043  pwrssmgc  33320  gsumwrd2dccatlem  33397  elrgspnsubrunlem2  33568  1fldgenq  33643  lindssn  33691  elrspunidl  33736  esplyfval1  33963  esplyfvaln  33964  lbslsat  34006  fldextrspunlsplem  34063  esumnul  34438  esumcst  34453  hashf2  34474  esum2d  34483  measvuni  34604  cntnevol  34618  eulerpartlemt  34761  eulerpartlemmf  34765  eulerpartlemgh  34768  ballotlemfp1  34882  reprinfz1  35009  fineqvac  35529  f1resfz0f1d  35605  dfon2lem3  36275  altxpsspw  36469  ttcmin  37027  ttcsnmin  37049  bj-snglss  37626  lindsadd  38284  lindsenlbs  38286  poimirlem16  38307  poimirlem19  38310  poimirlem23  38314  poimirlem25  38316  poimirlem29  38320  poimirlem31  38322  mblfinlem2  38329  dvasin  38375  fdc  38416  prnc  38738  isfldidl  38739  ispridlc  38741  islshpsm  39774  snatpsubN  40544  polatN  40725  atpsubclN  40739  pclfinclN  40744  readvrec2  43142  mapfzcons  43467  mzpcompact2lem  43502  diophrw  43510  brfvidRP  44434  cotrcltrcl  44471  corcltrcl  44485  cotrclrcl  44488  gneispa  44876  binomcxplemnotnn0  45086  snelpwrVD  45559  disjiun2  45798  infxrpnf  46180  mccllem  46333  islptre  46355  cncfdmsn  46624  snmbl  46697  stoweidlem44  46778  sge0tsms  47114  sge0iunmptlemfi  47147  ismeannd  47201  isomenndlem  47264  hoidmvlelem3  47331  hoidmvlelem4  47332  ovnhoilem1  47335  fnbrafvb  47911  afvres  47929  afv2res  47996  perfectALTVlem2  48507  mapsnop  49144  lincext2  49255  snlindsntorlem  49270  resinsnALT  49671  aacllem  50641