Theorem eqsn 4772

Description: Two ways to express that a nonempty set equals a singleton. (Contributed by NM, 15-Dec-2007.) (Proof shortened by JJ, 23-Jul-2021.)

Assertion

Ref	Expression
eqsn	⊢ (𝐴 ≠ ∅ → (𝐴 = {𝐵} ↔ ∀𝑥 ∈ 𝐴 𝑥 = 𝐵))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem eqsn

Step	Hyp	Ref	Expression
1		df-ne 2933	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅)
2		biorf 937	. . 3 ⊢ (¬ 𝐴 = ∅ → (𝐴 = {𝐵} ↔ (𝐴 = ∅ ∨ 𝐴 = {𝐵})))
3	1, 2	sylbi 217	. 2 ⊢ (𝐴 ≠ ∅ → (𝐴 = {𝐵} ↔ (𝐴 = ∅ ∨ 𝐴 = {𝐵})))
4		dfss3 3910	. . 3 ⊢ (𝐴 ⊆ {𝐵} ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ {𝐵})
5		sssn 4769	. . 3 ⊢ (𝐴 ⊆ {𝐵} ↔ (𝐴 = ∅ ∨ 𝐴 = {𝐵}))
6		velsn 4583	. . . 4 ⊢ (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵)
7	6	ralbii 3083	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ∈ {𝐵} ↔ ∀𝑥 ∈ 𝐴 𝑥 = 𝐵)
8	4, 5, 7	3bitr3i 301	. 2 ⊢ ((𝐴 = ∅ ∨ 𝐴 = {𝐵}) ↔ ∀𝑥 ∈ 𝐴 𝑥 = 𝐵)
9	3, 8	bitrdi 287	1 ⊢ (𝐴 ≠ ∅ → (𝐴 = {𝐵} ↔ ∀𝑥 ∈ 𝐴 𝑥 = 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∨ wo 848   = wceq 1542   ∈ wcel 2114   ≠ wne 2932  ∀wral 3051   ⊆ wss 3889  ∅c0 4273  {csn 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-v 3431  df-dif 3892  df-ss 3906  df-nul 4274  df-sn 4568

This theorem is referenced by:  eqsnd  4773  issn  4775  zornn0g  10427  hashgt12el  14384  hashgt12el2  14385  hashge2el2dif  14442  simpgnideld  20076  01eq0ring  20507  lssne0  20946  qtopeu  23681  n0nsnel  32585  dimval  33745  dimvalfi  33746  rngoueqz  38261  n0nsn2el  47473  lmod0rng  48705