Theorem snss 4719

Description: The singleton of an element of a class is a subset of the class (inference form of snssg 4718). Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 21-Jun-1993.)

Hypothesis

Ref	Expression
snss.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
snss	⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)

Proof of Theorem snss

Step	Hyp	Ref	Expression
1		snss.1	. 2 ⊢ 𝐴 ∈ V
2		snssg 4718	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)

Syntax hints:   ↔ wb 208   ∈ wcel 2121  Vcvv 3433   ⊆ wss 3885  {csn 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-ss 3902  df-sn 4559

This theorem is referenced by:  tpss  4771  sspwb  5391  nnullss  5404  exss  5405  pwssun  5513  fvimacnvi  6997  fvimacnv  6998  fvimacnvALT  7002  fnressn  7105  limensuci  9085  domunfican  9226  finsschain  9263  epfrs  9647  tc2  9656  tcsni  9657  dju1dif  10090  fpwwe2lem12  10560  wunfi  10639  uniwun  10658  un0mulcl  12466  nn0ssz  12542  xrinfmss  13257  hashbclem  14409  hashf1lem1  14412  hashf1lem2  14413  fsum2dlem  15727  fsumabs  15759  fsumrlim  15769  fsumo1  15770  fsumiun  15779  incexclem  15796  fprod2dlem  15940  lcmfunsnlem  16605  lcmfun  16609  coprmprod  16625  coprmproddvdslem  16626  ramcl2  16982  0ram  16986  strfv  17168  imasaddfnlem  17487  imasaddvallem  17488  acsfn1  17622  drsdirfi  18266  sylow2a  19589  gsumpt  19932  dprdfadd  19992  ablfac1eulem  20044  pgpfaclem1  20053  gsumle  20115  acsfn1p  20775  rsp1  21234  pzriprnglem4  21463  mplcoe1  22017  mplcoe5  22020  mdetunilem9  22607  opnnei  23107  iscnp4  23250  cnpnei  23251  hausnei2  23340  fiuncmp  23391  llycmpkgen2  23537  1stckgen  23541  ptbasfi  23568  xkoccn  23606  xkoptsub  23641  ptcmpfi  23800  cnextcn  24054  tsmsid  24127  ustuqtop3  24230  utopreg  24239  prdsdsf  24354  prdsmet  24357  prdsbl  24478  fsumcn  24859  itgfsum  25816  dvmptfsum  25964  elply2  26183  elplyd  26189  ply1term  26191  ply0  26195  plymullem  26203  jensenlem1  26972  jensenlem2  26973  frcond3  30361  h1de2bi  31647  spansni  31650  gsumvsca1  33311  gsumvsca2  33312  1fldgenq  33410  unitprodclb  33476  mxidlirredi  33558  extdg1id  33862  ordtconnlem1  34120  cntnevol  34424  eulerpartgbij  34568  breprexpnat  34830  cvmlift2lem1  35545  cvmlift2lem12  35557  dfon2lem7  36030  axtco  36714  bj-tagss  37348  lindsenlbs  37997  matunitlindflem1  37998  divrngidl  38410  isfldidl  38450  ispridlc  38452  pclfinclN  40457  osumcllem10N  40472  pexmidlem7N  40483  clsk1indlem4  44503  clsk1indlem1  44504  fourierdlem62  46625  nthrucw  47345