Theorem eqsn 4761

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 2935	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅)
2		biorf 942	. . 3 ⊢ (¬ 𝐴 = ∅ → (𝐴 = {𝐵} ↔ (𝐴 = ∅ ∨ 𝐴 = {𝐵})))
3	1, 2	sylbi 218	. 2 ⊢ (𝐴 ≠ ∅ → (𝐴 = {𝐵} ↔ (𝐴 = ∅ ∨ 𝐴 = {𝐵})))
4		dfss3 3904	. . 3 ⊢ (𝐴 ⊆ {𝐵} ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ {𝐵})
5		sssn 4758	. . 3 ⊢ (𝐴 ⊆ {𝐵} ↔ (𝐴 = ∅ ∨ 𝐴 = {𝐵}))
6		velsn 4572	. . . 4 ⊢ (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵)
7	6	ralbii 3085	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ∈ {𝐵} ↔ ∀𝑥 ∈ 𝐴 𝑥 = 𝐵)
8	4, 5, 7	3bitr3i 302	. 2 ⊢ ((𝐴 = ∅ ∨ 𝐴 = {𝐵}) ↔ ∀𝑥 ∈ 𝐴 𝑥 = 𝐵)
9	3, 8	bitrdi 288	1 ⊢ (𝐴 ≠ ∅ → (𝐴 = {𝐵} ↔ ∀𝑥 ∈ 𝐴 𝑥 = 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∨ wo 853   = wceq 1547   ∈ wcel 2119   ≠ wne 2934  ∀wral 3053   ⊆ wss 3883  ∅c0 4262  {csn 4556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-ral 3054  df-v 3433  df-dif 3886  df-ss 3900  df-nul 4263  df-sn 4557

This theorem is referenced by:  eqsnd  4762  issn  4764  zornn0g  10419  hashgt12el  14376  hashgt12el2  14377  hashge2el2dif  14434  simpgnideld  20068  01eq0ring  20503  lssne0  20942  qtopeu  23700  n0nsnel  32604  dimval  33794  dimvalfi  33795  rngoueqz  38316  n0nsn2el  47496  lmod0rng  48728