Theorem snssi 4717

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

Syntax hints:   → wi 4   ∈ wcel 2119   ⊆ wss 3883  {csn 4555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-ss 3900  df-sn 4556

This theorem is referenced by:  snssd  4718  difsnid  4741  eldifeldifsn  4742  pwpw0  4744  sssn  4757  ssunsn2  4758  tpssi  4769  frirr  5594  xpsspw  5752  djussxp  5787  dmressnsn  5975  fconst6g  6716  f1sng  6810  dffv2  6922  fvimacnvi  6993  fvimacnvALT  6998  fsn2  7078  fsnunf  7129  abnexg  7699  ordsuci  7751  curry1  8043  curry2  8046  xpord2pred  8085  xpord3pred  8092  ressuppss  8123  ressuppssdif  8125  naddcllem  8602  naddov2  8605  mapsnd  8824  ralxpmap  8834  fodomr  9056  findcard2  9089  findcard2s  9090  unfi  9095  ssfi  9097  sucdom2  9127  0sdom1dom  9146  enp1ilem  9178  fodomfir  9228  marypha1lem  9336  marypha2lem1  9338  epfrs  9643  dfac5lem4  10039  dfac5lem4OLD  10041  kmlem11  10074  ackbij1lem2  10133  fin23lem26  10238  isfin1-3  10299  hsmexlem4  10342  axdc3lem4  10366  axresscn  11062  nn0ssre  12432  nn0sscn  12433  xrsupss  13252  supxrmnf  13260  1exp  14044  hashxrcl  14310  hashdifsn  14367  hashdifsnp1  14459  repsdf2  14731  modfsummods  15747  fsum00  15752  incexc  15793  2ebits  16407  bitsinvp1  16409  lcmfunsnlem2lem1  16598  lcmfunsnlem2lem2  16599  lcmfunsnlem2  16600  coprmproddvdslem  16622  4sqlem19  16925  ramxrcl  16979  mrcsncl  17569  acsfn1  17618  homaf  17988  dmcoass  18024  lubel  18471  gsumws1  18797  eqg0subgecsn  19163  cycsubg2  19176  cntzsnval  19290  0frgp  19745  dpjidcl  20026  ablfac1eu  20041  lspsncl  20967  lspsnss  20980  lspsnid  20983  lpival  21317  lpiss  21322  lidldvgen  21327  pzriprnglem10  21465  znlidl  21508  frlmlbs  21772  mat1dimelbas  22454  smadiadetglem2  22655  isneip  23088  neips  23096  opnneip  23102  maxlp  23130  restsn2  23154  leordtval2  23195  ist1-3  23332  ordtt1  23362  2ndcdisj2  23440  uffix  23904  neiflim  23957  ptcmplem5  24039  cnextfres1  24051  haustsms2  24120  ust0  24203  ustuqtop5  24228  dscopn  24556  icccmplem1  24806  bndth  24943  ovolsn  25480  icombl1  25548  plyun0  26180  coeeulem  26207  coeeu  26208  vieta1lem2  26295  aalioulem2  26317  taylfval  26342  perfectlem2  27211  noextend  27648  noextendseq  27649  conway  27789  etaslts  27803  0lt1s  27822  sltsleft  27870  sltsright  27871  negsid  28051  precsexlem8  28224  precsexlem11  28227  n0bday  28362  elreno2  28505  istrkg2ld  28546  axlowdimlem7  29035  axlowdimlem10  29038  0clwlkv  30219  hsn0elch  31337  chsupsn  31502  chsup0  31637  h1deoi  31638  h1dei  31639  h1did  31640  h1de2ctlem  31644  h1de2ci  31645  spansni  31646  spansnch  31649  elspansncl  31654  spansnpji  31667  spanunsni  31668  spanpr  31669  h1datomi  31670  spansnji  31735  h1da  32438  atom1d  32442  superpos  32443  disjun0  32684  djussxp2  32740  mptprop  32790  pwrssmgc  33079  gsumwrd2dccatlem  33158  elrgspnsubrunlem2  33329  1fldgenq  33406  rspsnid  33454  lindssn  33461  elrspunidl  33511  esplyfval1  33757  esplyfvaln  33758  lbslsat  33800  fldextrspunlsplem  33857  esumnul  34232  esumcst  34247  hashf2  34268  esum2d  34277  measvuni  34398  cntnevol  34412  eulerpartlemt  34555  eulerpartlemmf  34559  eulerpartlemgh  34562  ballotlemfp1  34676  reprinfz1  34806  fineqvac  35297  f1resfz0f1d  35342  dfon2lem3  36011  altxpsspw  36205  ttcmin  36724  ttcsnmin  36746  bj-snglss  37323  lindsadd  37980  lindsenlbs  37982  poimirlem16  38003  poimirlem19  38006  poimirlem23  38010  poimirlem25  38012  poimirlem29  38016  poimirlem31  38018  mblfinlem2  38025  dvasin  38071  fdc  38112  prnc  38434  isfldidl  38435  ispridlc  38437  islshpsm  39472  snatpsubN  40242  polatN  40423  atpsubclN  40437  pclfinclN  40442  readvrec2  42838  mapfzcons  43165  mzpcompact2lem  43200  diophrw  43208  brfvidRP  44132  cotrcltrcl  44169  corcltrcl  44183  cotrclrcl  44186  gneispa  44574  binomcxplemnotnn0  44800  snelpwrVD  45274  disjiun2  45506  infxrpnf  45889  mccllem  46042  islptre  46064  cncfdmsn  46333  snmbl  46406  stoweidlem44  46487  sge0tsms  46823  sge0iunmptlemfi  46856  ismeannd  46910  isomenndlem  46973  hoidmvlelem3  47040  hoidmvlelem4  47041  ovnhoilem1  47044  fnbrafvb  47617  afvres  47635  afv2res  47702  perfectALTVlem2  48213  mapsnop  48835  lincext2  48946  snlindsntorlem  48961  resinsnALT  49363  aacllem  50291