Theorem sssn 4794

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 4306	. . . . . . 7 ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
2		ssel 3932	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ {𝐵} → (𝑥 ∈ 𝐴 → 𝑥 ∈ {𝐵}))
3		elsni 4608	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {𝐵} → 𝑥 = 𝐵)
4	2, 3	syl6 36	. . . . . . . . . 10 ⊢ (𝐴 ⊆ {𝐵} → (𝑥 ∈ 𝐴 → 𝑥 = 𝐵))
5		eleq1 2853	. . . . . . . . . 10 ⊢ (𝑥 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴))
6	4, 5	syl6 36	. . . . . . . . 9 ⊢ (𝐴 ⊆ {𝐵} → (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴)))
7	6	ibd 272	. . . . . . . 8 ⊢ (𝐴 ⊆ {𝐵} → (𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐴))
8	7	exlimdv 1966	. . . . . . 7 ⊢ (𝐴 ⊆ {𝐵} → (∃𝑥 𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐴))
9	1, 8	biimtrid 245	. . . . . 6 ⊢ (𝐴 ⊆ {𝐵} → (¬ 𝐴 = ∅ → 𝐵 ∈ 𝐴))
10		snssi 4753	. . . . . 6 ⊢ (𝐵 ∈ 𝐴 → {𝐵} ⊆ 𝐴)
11	9, 10	syl6 36	. . . . 5 ⊢ (𝐴 ⊆ {𝐵} → (¬ 𝐴 = ∅ → {𝐵} ⊆ 𝐴))
12	11	anc2li 565	. . . 4 ⊢ (𝐴 ⊆ {𝐵} → (¬ 𝐴 = ∅ → (𝐴 ⊆ {𝐵} ∧ {𝐵} ⊆ 𝐴)))
13		eqss 3953	. . . 4 ⊢ (𝐴 = {𝐵} ↔ (𝐴 ⊆ {𝐵} ∧ {𝐵} ⊆ 𝐴))
14	12, 13	imbitrrdi 255	. . 3 ⊢ (𝐴 ⊆ {𝐵} → (¬ 𝐴 = ∅ → 𝐴 = {𝐵}))
15	14	orrd 877	. 2 ⊢ (𝐴 ⊆ {𝐵} → (𝐴 = ∅ ∨ 𝐴 = {𝐵}))
16		0ss 4357	. . . 4 ⊢ ∅ ⊆ {𝐵}
17		sseq1 3963	. . . 4 ⊢ (𝐴 = ∅ → (𝐴 ⊆ {𝐵} ↔ ∅ ⊆ {𝐵}))
18	16, 17	mpbiri 261	. . 3 ⊢ (𝐴 = ∅ → 𝐴 ⊆ {𝐵})
19		eqimss 3996	. . 3 ⊢ (𝐴 = {𝐵} → 𝐴 ⊆ {𝐵})
20	18, 19	jaoi 871	. 2 ⊢ ((𝐴 = ∅ ∨ 𝐴 = {𝐵}) → 𝐴 ⊆ {𝐵})
21	15, 20	impbii 212	1 ⊢ (𝐴 ⊆ {𝐵} ↔ (𝐴 = ∅ ∨ 𝐴 = {𝐵}))

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1570  ∃wex 1812   ∈ wcel 2146   ⊆ wss 3906  ∅c0 4286  {csn 4591

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-dif 3909  df-ss 3923  df-nul 4287  df-sn 4592

This theorem is used by:  eqsn  4797  snsssn  4808  pwsn  4867  frsn  5751  foconst  6811  fin1a2lem12  10410  fpwwe2lem12  10642  gsumval2  18776  0top  23190  minveclem4a  25640  uvtx01vtx  29805  snsssng  32931  pmtrcnelor  33475  0ringsubrg  33635  lvecdim0  34061  locfinref  34295  ordcmp  37015  bj-snmoore  37812  nlpineqsn  38111  uneqsn  44809  mosssn  49650  mosssn2  49652  mofsssn  49681