Theorem sssn 4830

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 4357	. . . . . . 7 ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
2		ssel 3988	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ {𝐵} → (𝑥 ∈ 𝐴 → 𝑥 ∈ {𝐵}))
3		elsni 4647	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {𝐵} → 𝑥 = 𝐵)
4	2, 3	syl6 35	. . . . . . . . . 10 ⊢ (𝐴 ⊆ {𝐵} → (𝑥 ∈ 𝐴 → 𝑥 = 𝐵))
5		eleq1 2826	. . . . . . . . . 10 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴))
6	4, 5	syl6 35	. . . . . . . . 9 ⊢ (𝐴 ⊆ {𝐵} → (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴)))
7	6	ibd 269	. . . . . . . 8 ⊢ (𝐴 ⊆ {𝐵} → (𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐴))
8	7	exlimdv 1930	. . . . . . 7 ⊢ (𝐴 ⊆ {𝐵} → (∃𝑥 𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐴))
9	1, 8	biimtrid 242	. . . . . 6 ⊢ (𝐴 ⊆ {𝐵} → (¬ 𝐴 = ∅ → 𝐵 ∈ 𝐴))
10		snssi 4812	. . . . . 6 ⊢ (𝐵 ∈ 𝐴 → {𝐵} ⊆ 𝐴)
11	9, 10	syl6 35	. . . . 5 ⊢ (𝐴 ⊆ {𝐵} → (¬ 𝐴 = ∅ → {𝐵} ⊆ 𝐴))
12	11	anc2li 555	. . . 4 ⊢ (𝐴 ⊆ {𝐵} → (¬ 𝐴 = ∅ → (𝐴 ⊆ {𝐵} ∧ {𝐵} ⊆ 𝐴)))
13		eqss 4010	. . . 4 ⊢ (𝐴 = {𝐵} ↔ (𝐴 ⊆ {𝐵} ∧ {𝐵} ⊆ 𝐴))
14	12, 13	imbitrrdi 252	. . 3 ⊢ (𝐴 ⊆ {𝐵} → (¬ 𝐴 = ∅ → 𝐴 = {𝐵}))
15	14	orrd 863	. 2 ⊢ (𝐴 ⊆ {𝐵} → (𝐴 = ∅ ∨ 𝐴 = {𝐵}))
16		0ss 4405	. . . 4 ⊢ ∅ ⊆ {𝐵}
17		sseq1 4020	. . . 4 ⊢ (𝐴 = ∅ → (𝐴 ⊆ {𝐵} ↔ ∅ ⊆ {𝐵}))
18	16, 17	mpbiri 258	. . 3 ⊢ (𝐴 = ∅ → 𝐴 ⊆ {𝐵})
19		eqimss 4053	. . 3 ⊢ (𝐴 = {𝐵} → 𝐴 ⊆ {𝐵})
20	18, 19	jaoi 857	. 2 ⊢ ((𝐴 = ∅ ∨ 𝐴 = {𝐵}) → 𝐴 ⊆ {𝐵})
21	15, 20	impbii 209	1 ⊢ (𝐴 ⊆ {𝐵} ↔ (𝐴 = ∅ ∨ 𝐴 = {𝐵}))

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1536  ∃wex 1775   ∈ wcel 2105   ⊆ wss 3962  ∅c0 4338  {csn 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-dif 3965  df-ss 3979  df-nul 4339  df-sn 4631

This theorem is referenced by:  eqsn  4833  snsssn  4845  pwsn  4904  frsn  5775  foconst  6835  fin1a2lem12  10448  fpwwe2lem12  10679  gsumval2  18711  0top  23005  minveclem4a  25477  uvtx01vtx  29428  snsssng  32541  pmtrcnelor  33093  0ringsubrg  33237  lvecdim0  33633  locfinref  33801  ordcmp  36429  bj-snmoore  37095  nlpineqsn  37390  uneqsn  44014  mosssn  48662  mosssn2  48664  mofsssn  48675