Theorem sssn 4790

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 4315	. . . . . . 7 ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
2		ssel 3940	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ {𝐵} → (𝑥 ∈ 𝐴 → 𝑥 ∈ {𝐵}))
3		elsni 4606	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {𝐵} → 𝑥 = 𝐵)
4	2, 3	syl6 35	. . . . . . . . . 10 ⊢ (𝐴 ⊆ {𝐵} → (𝑥 ∈ 𝐴 → 𝑥 = 𝐵))
5		eleq1 2816	. . . . . . . . . 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 4772	. . . . . 6 ⊢ (𝐵 ∈ 𝐴 → {𝐵} ⊆ 𝐴)
11	9, 10	syl6 35	. . . . 5 ⊢ (𝐴 ⊆ {𝐵} → (¬ 𝐴 = ∅ → {𝐵} ⊆ 𝐴))
12	11	anc2li 555	. . . 4 ⊢ (𝐴 ⊆ {𝐵} → (¬ 𝐴 = ∅ → (𝐴 ⊆ {𝐵} ∧ {𝐵} ⊆ 𝐴)))
13		eqss 3962	. . . 4 ⊢ (𝐴 = {𝐵} ↔ (𝐴 ⊆ {𝐵} ∧ {𝐵} ⊆ 𝐴))
14	12, 13	imbitrrdi 252	. . 3 ⊢ (𝐴 ⊆ {𝐵} → (¬ 𝐴 = ∅ → 𝐴 = {𝐵}))
15	14	orrd 863	. 2 ⊢ (𝐴 ⊆ {𝐵} → (𝐴 = ∅ ∨ 𝐴 = {𝐵}))
16		0ss 4363	. . . 4 ⊢ ∅ ⊆ {𝐵}
17		sseq1 3972	. . . 4 ⊢ (𝐴 = ∅ → (𝐴 ⊆ {𝐵} ↔ ∅ ⊆ {𝐵}))
18	16, 17	mpbiri 258	. . 3 ⊢ (𝐴 = ∅ → 𝐴 ⊆ {𝐵})
19		eqimss 4005	. . 3 ⊢ (𝐴 = {𝐵} → 𝐴 ⊆ {𝐵})
20	18, 19	jaoi 857	. 2 ⊢ ((𝐴 = ∅ ∨ 𝐴 = {𝐵}) → 𝐴 ⊆ {𝐵})
21	15, 20	impbii 209	1 ⊢ (𝐴 ⊆ {𝐵} ↔ (𝐴 = ∅ ∨ 𝐴 = {𝐵}))

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1540  ∃wex 1779   ∈ wcel 2109   ⊆ wss 3914  ∅c0 4296  {csn 4589

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-dif 3917  df-ss 3931  df-nul 4297  df-sn 4590

This theorem is referenced by:  eqsn  4793  snsssn  4805  pwsn  4864  frsn  5726  foconst  6787  fin1a2lem12  10364  fpwwe2lem12  10595  gsumval2  18613  0top  22870  minveclem4a  25330  uvtx01vtx  29324  snsssng  32443  pmtrcnelor  33048  0ringsubrg  33202  lvecdim0  33602  locfinref  33831  ordcmp  36435  bj-snmoore  37101  nlpineqsn  37396  uneqsn  44014  mosssn  48803  mosssn2  48805  mofsssn  48834