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

Theorem sssn 4499
Description: The subsets of a singleton. (Contributed by NM, 24-Apr-2004.)
Assertion
Ref Expression
sssn (𝐴 ⊆ {𝐵} ↔ (𝐴 = ∅ ∨ 𝐴 = {𝐵}))

Proof of Theorem sssn
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 neq0 4069 . . . . . . 7 𝐴 = ∅ ↔ ∃𝑥 𝑥𝐴)
2 ssel 3734 . . . . . . . . . . 11 (𝐴 ⊆ {𝐵} → (𝑥𝐴𝑥 ∈ {𝐵}))
3 elsni 4334 . . . . . . . . . . 11 (𝑥 ∈ {𝐵} → 𝑥 = 𝐵)
42, 3syl6 35 . . . . . . . . . 10 (𝐴 ⊆ {𝐵} → (𝑥𝐴𝑥 = 𝐵))
5 eleq1 2823 . . . . . . . . . 10 (𝑥 = 𝐵 → (𝑥𝐴𝐵𝐴))
64, 5syl6 35 . . . . . . . . 9 (𝐴 ⊆ {𝐵} → (𝑥𝐴 → (𝑥𝐴𝐵𝐴)))
76ibd 258 . . . . . . . 8 (𝐴 ⊆ {𝐵} → (𝑥𝐴𝐵𝐴))
87exlimdv 2006 . . . . . . 7 (𝐴 ⊆ {𝐵} → (∃𝑥 𝑥𝐴𝐵𝐴))
91, 8syl5bi 232 . . . . . 6 (𝐴 ⊆ {𝐵} → (¬ 𝐴 = ∅ → 𝐵𝐴))
10 snssi 4480 . . . . . 6 (𝐵𝐴 → {𝐵} ⊆ 𝐴)
119, 10syl6 35 . . . . 5 (𝐴 ⊆ {𝐵} → (¬ 𝐴 = ∅ → {𝐵} ⊆ 𝐴))
1211anc2li 581 . . . 4 (𝐴 ⊆ {𝐵} → (¬ 𝐴 = ∅ → (𝐴 ⊆ {𝐵} ∧ {𝐵} ⊆ 𝐴)))
13 eqss 3755 . . . 4 (𝐴 = {𝐵} ↔ (𝐴 ⊆ {𝐵} ∧ {𝐵} ⊆ 𝐴))
1412, 13syl6ibr 242 . . 3 (𝐴 ⊆ {𝐵} → (¬ 𝐴 = ∅ → 𝐴 = {𝐵}))
1514orrd 392 . 2 (𝐴 ⊆ {𝐵} → (𝐴 = ∅ ∨ 𝐴 = {𝐵}))
16 0ss 4111 . . . 4 ∅ ⊆ {𝐵}
17 sseq1 3763 . . . 4 (𝐴 = ∅ → (𝐴 ⊆ {𝐵} ↔ ∅ ⊆ {𝐵}))
1816, 17mpbiri 248 . . 3 (𝐴 = ∅ → 𝐴 ⊆ {𝐵})
19 eqimss 3794 . . 3 (𝐴 = {𝐵} → 𝐴 ⊆ {𝐵})
2018, 19jaoi 393 . 2 ((𝐴 = ∅ ∨ 𝐴 = {𝐵}) → 𝐴 ⊆ {𝐵})
2115, 20impbii 199 1 (𝐴 ⊆ {𝐵} ↔ (𝐴 = ∅ ∨ 𝐴 = {𝐵}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wo 382  wa 383   = wceq 1628  wex 1849  wcel 2135  wss 3711  c0 4054  {csn 4317
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-v 3338  df-dif 3714  df-in 3718  df-ss 3725  df-nul 4055  df-sn 4318
This theorem is referenced by:  eqsn  4502  eqsnOLD  4503  snsssn  4513  pwsn  4576  frsn  5342  foconst  6283  fin1a2lem12  9421  fpwwe2lem13  9652  gsumval2  17477  0top  20985  minveclem4a  23397  uvtx01vtx  26496  uvtxa01vtx0OLD  26498  locfinref  30213  ordcmp  32748  bj-snmoore  33370  uneqsn  38819
  Copyright terms: Public domain W3C validator