Theorem snss 4748

Description: The singleton of an element of a class is a subset of the class (inference form of snssg 4747). 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 4747	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2145  Vcvv 3453   ⊆ wss 3902  {csn 4587

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-ss 3919  df-sn 4588

This theorem is used by:  tpss  4800  sspwb  5428  nnullss  5441  exss  5442  pwssun  5551  fvimacnvi  7048  fvimacnv  7049  fvimacnvALT  7053  fnressn  7159  limensuci  9155  domunfican  9295  finsschain  9330  epfrs  9714  tc2  9723  tcsni  9724  dju1dif  10179  fpwwe2lem12  10655  wunfi  10734  uniwun  10753  un0mulcl  12566  nn0ssz  12642  xrinfmss  13366  hashbclem  14521  hashf1lem1  14524  hashf1lem2  14525  fsum2dlem  15860  fsumabs  15892  fsumrlim  15902  fsumo1  15903  fsumiun  15912  incexclem  15929  fprod2dlem  16073  lcmfunsnlem  16737  lcmfun  16741  coprmprod  16757  coprmproddvdslem  16758  ramcl2  17114  0ram  17118  strfv  17301  imasaddfnlem  17620  imasaddvallem  17621  acsfn1  17755  drsdirfi  18399  sylow2a  19752  gsumpt  20095  dprdfadd  20155  ablfac1eulem  20207  pgpfaclem1  20216  gsumle  20278  acsfn1p  20971  rsp1  21435  pzriprnglem4  21703  lindsenlbs  22070  mplcoe1  22259  mplcoe5  22262  mdetunilem9  22848  matunitlindflem1  22907  opnnei  23351  iscnp4  23494  cnpnei  23495  hausnei2  23584  fiuncmp  23635  llycmpkgen2  23782  1stckgen  23786  ptbasfi  23813  xkoccn  23851  xkoptsub  23886  ptcmpfi  24045  cnextcn  24299  tsmsid  24372  ustuqtop3  24475  utopreg  24484  prdsdsf  24599  prdsmet  24602  prdsbl  24723  fsumcn  25104  itgfsum  26061  dvmptfsum  26209  elply2  26428  elplyd  26434  ply1term  26436  ply0  26440  plymullem  26449  jensenlem1  27231  jensenlem2  27232  frcond3  30757  h1de2bi  32043  spansni  32046  gsumvsca1  33674  gsumvsca2  33675  1fldgenq  33771  unitprodclb  33830  mxidlirredi  33882  extdg1id  34184  ordtconnlem1  34442  cntnevol  34747  eulerpartgbij  34891  breprexpnat  35150  cvmlift2lem1  35889  cvmlift2lem12  35901  dfon2lem7  36374  axtco  37098  bj-tagss  37732  divrngidl  38786  isfldidl  38826  ispridlc  38828  pclfinclN  40831  osumcllem10N  40846  pexmidlem7N  40857  clsk1indlem4  44892  clsk1indlem1  44893  fourierdlem62  47004  numtowerdt  47742