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

Theorem snssg 4709
Description: The singleton of an element of a class is a subset of the class (general form of snss 4710). 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 4573 . . . . 5 (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
21imbi1i 351 . . . 4 ((𝑥 ∈ {𝐴} → 𝑥𝐵) ↔ (𝑥 = 𝐴𝑥𝐵))
32albii 1811 . . 3 (∀𝑥(𝑥 ∈ {𝐴} → 𝑥𝐵) ↔ ∀𝑥(𝑥 = 𝐴𝑥𝐵))
43a1i 11 . 2 (𝐴𝑉 → (∀𝑥(𝑥 ∈ {𝐴} → 𝑥𝐵) ↔ ∀𝑥(𝑥 = 𝐴𝑥𝐵)))
5 dfss2 3952 . . 3 ({𝐴} ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝑥𝐵))
65a1i 11 . 2 (𝐴𝑉 → ({𝐴} ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝑥𝐵)))
7 clel2g 3649 . 2 (𝐴𝑉 → (𝐴𝐵 ↔ ∀𝑥(𝑥 = 𝐴𝑥𝐵)))
84, 6, 73bitr4rd 313 1 (𝐴𝑉 → (𝐴𝐵 ↔ {𝐴} ⊆ 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wal 1526   = wceq 1528  wcel 2105  wss 3933  {csn 4557
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-in 3940  df-ss 3949  df-sn 4558
This theorem is referenced by:  snss  4710  tppreqb  4730  snssi  4733  prssg  4744  relsng  5667  fvimacnvALT  6819  fr3nr  7483  vdwapid1  16299  acsfn  16918  cycsubg2  18291  cycsubg2cl  18292  pgpfac1lem1  19125  pgpfac1lem3a  19127  pgpfac1lem3  19128  pgpfac1lem5  19130  pgpfaclem2  19133  lspsnid  19694  lidldvgen  19956  isneip  21641  elnei  21647  iscnp4  21799  cnpnei  21800  nlly2i  22012  1stckgenlem  22089  flimopn  22511  flimclslem  22520  fclsneii  22553  fcfnei  22571  rrx0el  23928  limcvallem  24396  ellimc2  24402  limcflf  24406  limccnp  24416  limccnp2  24417  limcco  24418  lhop2  24539  plyrem  24821  isppw  25618  lpvtx  26780  h1did  29255  rspsnid  30864  erdszelem8  32342  neibastop2  33606  prnc  35226  proot1mul  39677  uneqsn  40251  mnuprdlem1  40485  islptre  41776  rrxsnicc  42462
  Copyright terms: Public domain W3C validator