Theorem snss 4259

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 4141	. . . 4 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2	1	imbi1i 338	. . 3 ⊢ ((𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵) ↔ (𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
3	2	albii 1737	. 2 ⊢ (∀𝑥(𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
4		dfss2 3557	. 2 ⊢ ({𝐴} ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵))
5		snss.1	. . 3 ⊢ 𝐴 ∈ V
6	5	clel2 3309	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
7	3, 4, 6	3bitr4ri 292	1 ⊢ (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)

Syntax hints:   → wi 4   ↔ wb 195  ∀wal 1473   = wceq 1475   ∈ wcel 1977  Vcvv 3173   ⊆ wss 3540  {csn 4125

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554  df-sn 4126

This theorem is referenced by:  snssg  4268  prssOLD  4292  tpss  4304  snelpw  4835  sspwb  4838  nnullss  4851  exss  4852  pwssun  4934  relsn  5135  fvimacnvi  6224  fvimacnv  6225  fvimacnvALT  6229  fnressn  6308  limensuci  7999  domunfican  8096  finsschain  8134  epfrs  8468  tc2  8479  tcsni  8480  cda1dif  8859  fpwwe2lem13  9321  wunfi  9400  uniwun  9419  un0mulcl  11177  nn0ssz  11234  xrinfmss  11971  hashbclem  13048  hashf1lem1  13051  hashf1lem2  13052  fsum2dlem  14292  fsumabs  14323  fsumrlim  14333  fsumo1  14334  fsumiun  14343  incexclem  14356  fprod2dlem  14498  lcmfunsnlem  15141  lcmfun  15145  coprmprod  15162  coprmproddvdslem  15163  ramcl2  15507  0ram  15511  strfv  15684  imasaddfnlem  15960  imasaddvallem  15961  acsfn1  16094  drsdirfi  16710  sylow2a  17806  gsumpt  18133  dprdfadd  18191  ablfac1eulem  18243  pgpfaclem1  18252  rsp1  18994  mplcoe1  19235  mplcoe5  19238  mdetunilem9  20193  opnnei  20682  iscnp4  20825  cnpnei  20826  hausnei2  20915  fiuncmp  20965  llycmpkgen2  21111  1stckgen  21115  ptbasfi  21142  xkoccn  21180  xkoptsub  21215  ptcmpfi  21374  cnextcn  21629  tsmsid  21701  ustuqtop3  21805  utopreg  21814  prdsdsf  21930  prdsmet  21933  prdsbl  22054  fsumcn  22429  itgfsum  23344  dvmptfsum  23487  elply2  23701  elplyd  23707  ply1term  23709  ply0  23713  plymullem  23721  jensenlem1  24458  jensenlem2  24459  frisusgranb  26318  h1de2bi  27591  spansni  27594  gsumle  28904  gsumvsca1  28907  gsumvsca2  28908  ordtconlem1  29092  cntnevol  29412  eulerpartgbij  29555  cvmlift2lem1  30332  cvmlift2lem12  30344  dfon2lem7  30732  bj-tagss  31955  lindsenlbs  32368  matunitlindflem1  32369  divrngidl  32791  isfldidl  32831  ispridlc  32833  pclfinclN  34048  osumcllem10N  34063  pexmidlem7N  34074  acsfn1p  36582  clsk1indlem4  37156  clsk1indlem1  37157  fourierdlem62  38855  frcond3  41432