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

Theorem sssn 4826
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 4352 . . . . . . 7 𝐴 = ∅ ↔ ∃𝑥 𝑥𝐴)
2 ssel 3977 . . . . . . . . . . 11 (𝐴 ⊆ {𝐵} → (𝑥𝐴𝑥 ∈ {𝐵}))
3 elsni 4643 . . . . . . . . . . 11 (𝑥 ∈ {𝐵} → 𝑥 = 𝐵)
42, 3syl6 35 . . . . . . . . . 10 (𝐴 ⊆ {𝐵} → (𝑥𝐴𝑥 = 𝐵))
5 eleq1 2829 . . . . . . . . . 10 (𝑥 = 𝐵 → (𝑥𝐴𝐵𝐴))
64, 5syl6 35 . . . . . . . . 9 (𝐴 ⊆ {𝐵} → (𝑥𝐴 → (𝑥𝐴𝐵𝐴)))
76ibd 269 . . . . . . . 8 (𝐴 ⊆ {𝐵} → (𝑥𝐴𝐵𝐴))
87exlimdv 1933 . . . . . . 7 (𝐴 ⊆ {𝐵} → (∃𝑥 𝑥𝐴𝐵𝐴))
91, 8biimtrid 242 . . . . . 6 (𝐴 ⊆ {𝐵} → (¬ 𝐴 = ∅ → 𝐵𝐴))
10 snssi 4808 . . . . . 6 (𝐵𝐴 → {𝐵} ⊆ 𝐴)
119, 10syl6 35 . . . . 5 (𝐴 ⊆ {𝐵} → (¬ 𝐴 = ∅ → {𝐵} ⊆ 𝐴))
1211anc2li 555 . . . 4 (𝐴 ⊆ {𝐵} → (¬ 𝐴 = ∅ → (𝐴 ⊆ {𝐵} ∧ {𝐵} ⊆ 𝐴)))
13 eqss 3999 . . . 4 (𝐴 = {𝐵} ↔ (𝐴 ⊆ {𝐵} ∧ {𝐵} ⊆ 𝐴))
1412, 13imbitrrdi 252 . . 3 (𝐴 ⊆ {𝐵} → (¬ 𝐴 = ∅ → 𝐴 = {𝐵}))
1514orrd 864 . 2 (𝐴 ⊆ {𝐵} → (𝐴 = ∅ ∨ 𝐴 = {𝐵}))
16 0ss 4400 . . . 4 ∅ ⊆ {𝐵}
17 sseq1 4009 . . . 4 (𝐴 = ∅ → (𝐴 ⊆ {𝐵} ↔ ∅ ⊆ {𝐵}))
1816, 17mpbiri 258 . . 3 (𝐴 = ∅ → 𝐴 ⊆ {𝐵})
19 eqimss 4042 . . 3 (𝐴 = {𝐵} → 𝐴 ⊆ {𝐵})
2018, 19jaoi 858 . 2 ((𝐴 = ∅ ∨ 𝐴 = {𝐵}) → 𝐴 ⊆ {𝐵})
2115, 20impbii 209 1 (𝐴 ⊆ {𝐵} ↔ (𝐴 = ∅ ∨ 𝐴 = {𝐵}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 206  wa 395  wo 848   = wceq 1540  wex 1779  wcel 2108  wss 3951  c0 4333  {csn 4626
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954  df-ss 3968  df-nul 4334  df-sn 4627
This theorem is referenced by:  eqsn  4829  snsssn  4841  pwsn  4900  frsn  5773  foconst  6835  fin1a2lem12  10451  fpwwe2lem12  10682  gsumval2  18699  0top  22990  minveclem4a  25464  uvtx01vtx  29414  snsssng  32533  pmtrcnelor  33111  0ringsubrg  33255  lvecdim0  33657  locfinref  33840  ordcmp  36448  bj-snmoore  37114  nlpineqsn  37409  uneqsn  44038  mosssn  48734  mosssn2  48736  mofsssn  48755
  Copyright terms: Public domain W3C validator