Theorem snss 4316

Description: The singleton of an element of a class is a subset of the class. 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

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		velsn 4193	. . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2	1	imbi1i 339	. . 3 ⊢ ((𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵) ↔ (𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
3	2	albii 1747	. 2 ⊢ (∀𝑥(𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
4		dfss2 3591	. 2 ⊢ ({𝐴} ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵))
5		snss.1	. . 3 ⊢ 𝐴 ∈ V
6	5	clel2 3339	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
7	3, 4, 6	3bitr4ri 293	1 ⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)

Syntax hints:   → wi 4   ↔ wb 196  ∀wal 1481   = wceq 1483   ∈ wcel 1990  Vcvv 3200   ⊆ wss 3574  {csn 4177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-ss 3588  df-sn 4178

This theorem is referenced by:  snssg  4327  prssOLD  4352  tpss  4368  snelpw  4913  sspwb  4917  nnullss  4930  exss  4931  pwssun  5020  relsn  5223  fvimacnvi  6331  fvimacnv  6332  fvimacnvALT  6336  fnressn  6425  limensuci  8136  domunfican  8233  finsschain  8273  epfrs  8607  tc2  8618  tcsni  8619  cda1dif  8998  fpwwe2lem13  9464  wunfi  9543  uniwun  9562  un0mulcl  11327  nn0ssz  11398  xrinfmss  12140  hashbclem  13236  hashf1lem1  13239  hashf1lem2  13240  fsum2dlem  14501  fsumabs  14533  fsumrlim  14543  fsumo1  14544  fsumiun  14553  incexclem  14568  fprod2dlem  14710  lcmfunsnlem  15354  lcmfun  15358  coprmprod  15375  coprmproddvdslem  15376  ramcl2  15720  0ram  15724  strfv  15907  imasaddfnlem  16188  imasaddvallem  16189  acsfn1  16322  drsdirfi  16938  sylow2a  18034  gsumpt  18361  dprdfadd  18419  ablfac1eulem  18471  pgpfaclem1  18480  rsp1  19224  mplcoe1  19465  mplcoe5  19468  mdetunilem9  20426  opnnei  20924  iscnp4  21067  cnpnei  21068  hausnei2  21157  fiuncmp  21207  llycmpkgen2  21353  1stckgen  21357  ptbasfi  21384  xkoccn  21422  xkoptsub  21457  ptcmpfi  21616  cnextcn  21871  tsmsid  21943  ustuqtop3  22047  utopreg  22056  prdsdsf  22172  prdsmet  22175  prdsbl  22296  fsumcn  22673  itgfsum  23593  dvmptfsum  23738  elply2  23952  elplyd  23958  ply1term  23960  ply0  23964  plymullem  23972  jensenlem1  24713  jensenlem2  24714  frcond3  27133  h1de2bi  28413  spansni  28416  gsumle  29779  gsumvsca1  29782  gsumvsca2  29783  ordtconnlem1  29970  cntnevol  30291  eulerpartgbij  30434  breprexpnat  30712  cvmlift2lem1  31284  cvmlift2lem12  31296  dfon2lem7  31694  bj-tagss  32968  lindsenlbs  33404  matunitlindflem1  33405  divrngidl  33827  isfldidl  33867  ispridlc  33869  pclfinclN  35236  osumcllem10N  35251  pexmidlem7N  35262  acsfn1p  37769  clsk1indlem4  38342  clsk1indlem1  38343  fourierdlem62  40385