Theorem eqsn 4789

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 2926	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅)
2		biorf 936	. . 3 ⊢ (¬ 𝐴 = ∅ → (𝐴 = {𝐵} ↔ (𝐴 = ∅ ∨ 𝐴 = {𝐵})))
3	1, 2	sylbi 217	. 2 ⊢ (𝐴 ≠ ∅ → (𝐴 = {𝐵} ↔ (𝐴 = ∅ ∨ 𝐴 = {𝐵})))
4		dfss3 3932	. . 3 ⊢ (𝐴 ⊆ {𝐵} ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ {𝐵})
5		sssn 4786	. . 3 ⊢ (𝐴 ⊆ {𝐵} ↔ (𝐴 = ∅ ∨ 𝐴 = {𝐵}))
6		velsn 4601	. . . 4 ⊢ (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵)
7	6	ralbii 3075	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ∈ {𝐵} ↔ ∀𝑥 ∈ 𝐴 𝑥 = 𝐵)
8	4, 5, 7	3bitr3i 301	. 2 ⊢ ((𝐴 = ∅ ∨ 𝐴 = {𝐵}) ↔ ∀𝑥 ∈ 𝐴 𝑥 = 𝐵)
9	3, 8	bitrdi 287	1 ⊢ (𝐴 ≠ ∅ → (𝐴 = {𝐵} ↔ ∀𝑥 ∈ 𝐴 𝑥 = 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∨ wo 847   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044   ⊆ wss 3911  ∅c0 4292  {csn 4585

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-ne 2926  df-ral 3045  df-v 3446  df-dif 3914  df-ss 3928  df-nul 4293  df-sn 4586

This theorem is referenced by:  eqsnd  4790  issn  4792  zornn0g  10434  hashgt12el  14363  hashgt12el2  14364  hashge2el2dif  14421  simpgnideld  20015  01eq0ring  20450  lssne0  20889  qtopeu  23636  n0nsnel  32494  dimval  33589  dimvalfi  33590  rngoueqz  37927  n0nsn2el  47019  lmod0rng  48210