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

Theorem snssg 4624
Description: The singleton of an element of a class is a subset of the class (general form of snss 4625). 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 4488 . . . . 5 (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
21imbi1i 351 . . . 4 ((𝑥 ∈ {𝐴} → 𝑥𝐵) ↔ (𝑥 = 𝐴𝑥𝐵))
32albii 1801 . . 3 (∀𝑥(𝑥 ∈ {𝐴} → 𝑥𝐵) ↔ ∀𝑥(𝑥 = 𝐴𝑥𝐵))
43a1i 11 . 2 (𝐴𝑉 → (∀𝑥(𝑥 ∈ {𝐴} → 𝑥𝐵) ↔ ∀𝑥(𝑥 = 𝐴𝑥𝐵)))
5 dfss2 3877 . . 3 ({𝐴} ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝑥𝐵))
65a1i 11 . 2 (𝐴𝑉 → ({𝐴} ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝑥𝐵)))
7 clel2g 3590 . 2 (𝐴𝑉 → (𝐴𝐵 ↔ ∀𝑥(𝑥 = 𝐴𝑥𝐵)))
84, 6, 73bitr4rd 313 1 (𝐴𝑉 → (𝐴𝐵 ↔ {𝐴} ⊆ 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wal 1520   = wceq 1522  wcel 2081  wss 3859  {csn 4472
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-v 3439  df-in 3866  df-ss 3874  df-sn 4473
This theorem is referenced by:  snss  4625  tppreqb  4645  snssi  4648  prssg  4659  relsng  5560  fvimacnvALT  6692  fr3nr  7350  vdwapid1  16140  acsfn  16759  cycsubg2  18070  cycsubg2cl  18071  pgpfac1lem1  18913  pgpfac1lem3a  18915  pgpfac1lem3  18916  pgpfac1lem5  18918  pgpfaclem2  18921  lspsnid  19455  lidldvgen  19717  isneip  21397  elnei  21403  iscnp4  21555  cnpnei  21556  nlly2i  21768  1stckgenlem  21845  flimopn  22267  flimclslem  22276  fclsneii  22309  fcfnei  22327  rrx0el  23684  limcvallem  24152  ellimc2  24158  limcflf  24162  limccnp  24172  limccnp2  24173  limcco  24174  lhop2  24295  plyrem  24577  isppw  25373  lpvtx  26536  h1did  29019  erdszelem8  32053  neibastop2  33318  prnc  34877  proot1mul  39284  uneqsn  39858  mnuprdlem1  40105  islptre  41442  rrxsnicc  42127
  Copyright terms: Public domain W3C validator