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.

Step	Hyp	Ref	Expression
1		neq0 4352	. . . . . . 7 ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
2		ssel 3977	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ {𝐵} → (𝑥 ∈ 𝐴 → 𝑥 ∈ {𝐵}))
3		elsni 4643	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {𝐵} → 𝑥 = 𝐵)
4	2, 3	syl6 35	. . . . . . . . . 10 ⊢ (𝐴 ⊆ {𝐵} → (𝑥 ∈ 𝐴 → 𝑥 = 𝐵))
5		eleq1 2829	. . . . . . . . . 10 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴))
6	4, 5	syl6 35	. . . . . . . . 9 ⊢ (𝐴 ⊆ {𝐵} → (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴)))
7	6	ibd 269	. . . . . . . 8 ⊢ (𝐴 ⊆ {𝐵} → (𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐴))
8	7	exlimdv 1933	. . . . . . 7 ⊢ (𝐴 ⊆ {𝐵} → (∃𝑥 𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐴))
9	1, 8	biimtrid 242	. . . . . 6 ⊢ (𝐴 ⊆ {𝐵} → (¬ 𝐴 = ∅ → 𝐵 ∈ 𝐴))
10		snssi 4808	. . . . . 6 ⊢ (𝐵 ∈ 𝐴 → {𝐵} ⊆ 𝐴)
11	9, 10	syl6 35	. . . . 5 ⊢ (𝐴 ⊆ {𝐵} → (¬ 𝐴 = ∅ → {𝐵} ⊆ 𝐴))
12	11	anc2li 555	. . . 4 ⊢ (𝐴 ⊆ {𝐵} → (¬ 𝐴 = ∅ → (𝐴 ⊆ {𝐵} ∧ {𝐵} ⊆ 𝐴)))
13		eqss 3999	. . . 4 ⊢ (𝐴 = {𝐵} ↔ (𝐴 ⊆ {𝐵} ∧ {𝐵} ⊆ 𝐴))
14	12, 13	imbitrrdi 252	. . 3 ⊢ (𝐴 ⊆ {𝐵} → (¬ 𝐴 = ∅ → 𝐴 = {𝐵}))
15	14	orrd 864	. 2 ⊢ (𝐴 ⊆ {𝐵} → (𝐴 = ∅ ∨ 𝐴 = {𝐵}))
16		0ss 4400	. . . 4 ⊢ ∅ ⊆ {𝐵}
17		sseq1 4009	. . . 4 ⊢ (𝐴 = ∅ → (𝐴 ⊆ {𝐵} ↔ ∅ ⊆ {𝐵}))
18	16, 17	mpbiri 258	. . 3 ⊢ (𝐴 = ∅ → 𝐴 ⊆ {𝐵})
19		eqimss 4042	. . 3 ⊢ (𝐴 = {𝐵} → 𝐴 ⊆ {𝐵})
20	18, 19	jaoi 858	. 2 ⊢ ((𝐴 = ∅ ∨ 𝐴 = {𝐵}) → 𝐴 ⊆ {𝐵})
21	15, 20	impbii 209	1 ⊢ (𝐴 ⊆ {𝐵} ↔ (𝐴 = ∅ ∨ 𝐴 = {𝐵}))

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