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

Theorem snssg 4678
 Description: The singleton of an element of a class is a subset of the class (general form of snss 4679). Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 22-Jul-2001.)
Assertion
Ref Expression
snssg (𝐴𝑉 → (𝐴𝐵 ↔ {𝐴} ⊆ 𝐵))

Proof of Theorem snssg
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 velsn 4541 . . . . 5 (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
21imbi1i 353 . . . 4 ((𝑥 ∈ {𝐴} → 𝑥𝐵) ↔ (𝑥 = 𝐴𝑥𝐵))
32albii 1821 . . 3 (∀𝑥(𝑥 ∈ {𝐴} → 𝑥𝐵) ↔ ∀𝑥(𝑥 = 𝐴𝑥𝐵))
43a1i 11 . 2 (𝐴𝑉 → (∀𝑥(𝑥 ∈ {𝐴} → 𝑥𝐵) ↔ ∀𝑥(𝑥 = 𝐴𝑥𝐵)))
5 dfss2 3901 . . 3 ({𝐴} ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝑥𝐵))
65a1i 11 . 2 (𝐴𝑉 → ({𝐴} ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝑥𝐵)))
7 clel2g 3600 . 2 (𝐴𝑉 → (𝐴𝐵 ↔ ∀𝑥(𝑥 = 𝐴𝑥𝐵)))
84, 6, 73bitr4rd 315 1 (𝐴𝑉 → (𝐴𝐵 ↔ {𝐴} ⊆ 𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1536   = wceq 1538   ∈ wcel 2111   ⊆ wss 3881  {csn 4525 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-sn 4526 This theorem is referenced by:  snss  4679  tppreqb  4698  snssi  4701  prssg  4712  relsng  5639  fvimacnvALT  6805  fr3nr  7477  vdwapid1  16304  acsfn  16925  cycsubg2  18349  cycsubg2cl  18350  pgpfac1lem1  19193  pgpfac1lem3a  19195  pgpfac1lem3  19196  pgpfac1lem5  19198  pgpfaclem2  19201  lspsnid  19762  lidldvgen  20025  isneip  21720  elnei  21726  iscnp4  21878  cnpnei  21879  nlly2i  22091  1stckgenlem  22168  flimopn  22590  flimclslem  22599  fclsneii  22632  fcfnei  22650  rrx0el  24012  limcvallem  24484  ellimc2  24490  limcflf  24494  limccnp  24504  limccnp2  24505  limcco  24506  lhop2  24628  plyrem  24911  isppw  25709  lpvtx  26871  h1did  29344  rspsnid  30998  erdszelem8  32573  neibastop2  33837  prnc  35524  proot1mul  40186  uneqsn  40769  mnuprdlem1  41023  islptre  42304  rrxsnicc  42985
 Copyright terms: Public domain W3C validator