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

Theorem snssg 4451
Description: The singleton of an element of a class is a subset of the class (general form of snss 4452). 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 4333 . . . . 5 (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
21imbi1i 338 . . . 4 ((𝑥 ∈ {𝐴} → 𝑥𝐵) ↔ (𝑥 = 𝐴𝑥𝐵))
32albii 1895 . . 3 (∀𝑥(𝑥 ∈ {𝐴} → 𝑥𝐵) ↔ ∀𝑥(𝑥 = 𝐴𝑥𝐵))
43a1i 11 . 2 (𝐴𝑉 → (∀𝑥(𝑥 ∈ {𝐴} → 𝑥𝐵) ↔ ∀𝑥(𝑥 = 𝐴𝑥𝐵)))
5 dfss2 3740 . . 3 ({𝐴} ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝑥𝐵))
65a1i 11 . 2 (𝐴𝑉 → ({𝐴} ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝑥𝐵)))
7 clel2g 3489 . 2 (𝐴𝑉 → (𝐴𝐵 ↔ ∀𝑥(𝑥 = 𝐴𝑥𝐵)))
84, 6, 73bitr4rd 301 1 (𝐴𝑉 → (𝐴𝐵 ↔ {𝐴} ⊆ 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1629   = wceq 1631  wcel 2145  wss 3723  {csn 4317
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-in 3730  df-ss 3737  df-sn 4318
This theorem is referenced by:  snss  4452  tppreqb  4472  snssi  4475  prssg  4486  relsng  5362  fvimacnvALT  6481  fr3nr  7130  vdwapid1  15886  acsfn  16527  cycsubg2  17839  cycsubg2cl  17840  pgpfac1lem1  18681  pgpfac1lem3a  18683  pgpfac1lem3  18684  pgpfac1lem5  18686  pgpfaclem2  18689  lspsnid  19206  lidldvgen  19470  isneip  21130  elnei  21136  iscnp4  21288  cnpnei  21289  nlly2i  21500  1stckgenlem  21577  flimopn  21999  flimclslem  22008  fclsneii  22041  fcfnei  22059  limcvallem  23855  ellimc2  23861  limcflf  23865  limccnp  23875  limccnp2  23876  limcco  23877  lhop2  23998  plyrem  24280  isppw  25061  lpvtx  26184  h1did  28750  erdszelem8  31518  neibastop2  32693  prnc  34196  proot1mul  38301  uneqsn  38845  islptre  40364  rrxsnicc  41032
  Copyright terms: Public domain W3C validator