Theorem elsng 4598

Description: There is exactly one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15 (generalized). (Contributed by NM, 13-Sep-1995.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)

Assertion

Ref	Expression
elsng	⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))

Proof of Theorem elsng

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq1 2765	. 2 ⊢ (𝑥 = 𝐴 → (𝑥 = 𝐵 ↔ 𝐴 = 𝐵))
2		df-sn 4585	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
3	1, 2	elab2g 3634	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145  {csn 4584

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-sn 4585

This theorem is used by:  elsn  4599  elsni  4601  snidg  4621  elunsn  4644  eltpg  4647  el7g  4651  eldifsn  4748  sneqrg  4799  elsucg  6432  ltxr  13237  elfzp12  13730  fzdif1  13732  fprodn0f  16151  lcmfunsnlem2  16808  ramcl  17200  initoeu2lem1  18182  pmtrdifellem4  19686  psdmul  22480  plymulidp  26596  logbmpt  27109  2lgslem2  27715  xrge0tsmsbi  33628  rprmnz  34045  dimkerim  34252  elzrhunit  34602  esumrnmpt2  34693  bj-projval  37889  bj-elsn12g  37955  bj-elsnb  37956  bj-snmoore  38014  bj-elsn0  38056  eldmressnALTV  39191  brressn  39443  zndvdchrrhm  43003  aks4d1p6  43111  aks6d1c2lem4  43157  sticksstones11  43186  aks6d1c6lem2  43201  aks6d1c7lem1  43210  rhmqusspan  43215  unitscyglem2  43226  reclimc  46632  itgsincmulx  46953  dirkercncflem2  47083  dirkercncflem4  47085  fourierdlem53  47138  fourierdlem58  47143  fourierdlem60  47145  fourierdlem61  47146  fourierdlem62  47147  fourierdlem76  47161  fourierdlem101  47186  elaa2  47213  etransc  47262  qndenserrnbl  47274  sge0tsms  47359  el1fzopredsuc  48365  elclnbgrelnbgr  48892  clnbupgrel  48901  mndtcob  50659