Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  snss Structured version   Visualization version   GIF version

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.
StepHypRef Expression
1 velsn 4141 . . . 4 (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
21imbi1i 338 . . 3 ((𝑥 ∈ {𝐴} → 𝑥𝐵) ↔ (𝑥 = 𝐴𝑥𝐵))
32albii 1737 . 2 (∀𝑥(𝑥 ∈ {𝐴} → 𝑥𝐵) ↔ ∀𝑥(𝑥 = 𝐴𝑥𝐵))
4 dfss2 3557 . 2 ({𝐴} ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝑥𝐵))
5 snss.1 . . 3 𝐴 ∈ V
65clel2 3309 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥 = 𝐴𝑥𝐵))
73, 4, 63bitr4ri 292 1 (𝐴𝐵 ↔ {𝐴} ⊆ 𝐵)
 Colors of variables: wff setvar class 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  4308  snelpw  4840  sspwb  4844  nnullss  4857  exss  4858  pwssun  4944  relsn  5146  fvimacnvi  6239  fvimacnv  6240  fvimacnvALT  6244  fnressn  6330  limensuci  8021  domunfican  8118  finsschain  8156  epfrs  8490  tc2  8501  tcsni  8502  cda1dif  8881  fpwwe2lem13  9343  wunfi  9422  uniwun  9441  un0mulcl  11204  nn0ssz  11275  xrinfmss  12012  hashbclem  13093  hashf1lem1  13096  hashf1lem2  13097  fsum2dlem  14343  fsumabs  14374  fsumrlim  14384  fsumo1  14385  fsumiun  14394  incexclem  14407  fprod2dlem  14549  lcmfunsnlem  15192  lcmfun  15196  coprmprod  15213  coprmproddvdslem  15214  ramcl2  15558  0ram  15562  strfv  15735  imasaddfnlem  16011  imasaddvallem  16012  acsfn1  16145  drsdirfi  16761  sylow2a  17857  gsumpt  18184  dprdfadd  18242  ablfac1eulem  18294  pgpfaclem1  18303  rsp1  19045  mplcoe1  19286  mplcoe5  19289  mdetunilem9  20245  opnnei  20734  iscnp4  20877  cnpnei  20878  hausnei2  20967  fiuncmp  21017  llycmpkgen2  21163  1stckgen  21167  ptbasfi  21194  xkoccn  21232  xkoptsub  21267  ptcmpfi  21426  cnextcn  21681  tsmsid  21753  ustuqtop3  21857  utopreg  21866  prdsdsf  21982  prdsmet  21985  prdsbl  22106  fsumcn  22481  itgfsum  23399  dvmptfsum  23542  elply2  23756  elplyd  23762  ply1term  23764  ply0  23768  plymullem  23776  jensenlem1  24513  jensenlem2  24514  frisusgranb  26524  h1de2bi  27797  spansni  27800  gsumle  29110  gsumvsca1  29113  gsumvsca2  29114  ordtconlem1  29298  cntnevol  29618  eulerpartgbij  29761  cvmlift2lem1  30538  cvmlift2lem12  30550  dfon2lem7  30938  bj-tagss  32161  lindsenlbs  32574  matunitlindflem1  32575  divrngidl  32997  isfldidl  33037  ispridlc  33039  pclfinclN  34254  osumcllem10N  34269  pexmidlem7N  34280  acsfn1p  36788  clsk1indlem4  37362  clsk1indlem1  37363  fourierdlem62  39061  frcond3  41440
 Copyright terms: Public domain W3C validator