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

Theorem snssg 4469
Description: The singleton of an element of a class is a subset of the class (general form of snss 4470). 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 4350 . . . . 5 (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
21imbi1i 340 . . . 4 ((𝑥 ∈ {𝐴} → 𝑥𝐵) ↔ (𝑥 = 𝐴𝑥𝐵))
32albii 1914 . . 3 (∀𝑥(𝑥 ∈ {𝐴} → 𝑥𝐵) ↔ ∀𝑥(𝑥 = 𝐴𝑥𝐵))
43a1i 11 . 2 (𝐴𝑉 → (∀𝑥(𝑥 ∈ {𝐴} → 𝑥𝐵) ↔ ∀𝑥(𝑥 = 𝐴𝑥𝐵)))
5 dfss2 3749 . . 3 ({𝐴} ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝑥𝐵))
65a1i 11 . 2 (𝐴𝑉 → ({𝐴} ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝑥𝐵)))
7 clel2g 3492 . 2 (𝐴𝑉 → (𝐴𝐵 ↔ ∀𝑥(𝑥 = 𝐴𝑥𝐵)))
84, 6, 73bitr4rd 303 1 (𝐴𝑉 → (𝐴𝐵 ↔ {𝐴} ⊆ 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wal 1650   = wceq 1652  wcel 2155  wss 3732  {csn 4334
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-v 3352  df-in 3739  df-ss 3746  df-sn 4335
This theorem is referenced by:  snss  4470  tppreqb  4490  snssi  4493  prssg  4504  relsng  5392  fvimacnvALT  6526  fr3nr  7177  vdwapid1  15958  acsfn  16585  cycsubg2  17895  cycsubg2cl  17896  pgpfac1lem1  18740  pgpfac1lem3a  18742  pgpfac1lem3  18743  pgpfac1lem5  18745  pgpfaclem2  18748  lspsnid  19265  lidldvgen  19529  isneip  21189  elnei  21195  iscnp4  21347  cnpnei  21348  nlly2i  21559  1stckgenlem  21636  flimopn  22058  flimclslem  22067  fclsneii  22100  fcfnei  22118  limcvallem  23926  ellimc2  23932  limcflf  23936  limccnp  23946  limccnp2  23947  limcco  23948  lhop2  24069  plyrem  24351  isppw  25131  lpvtx  26240  h1did  28866  erdszelem8  31628  neibastop2  32799  prnc  34288  proot1mul  38454  uneqsn  38995  islptre  40489  rrxsnicc  41157
  Copyright terms: Public domain W3C validator