Theorem elsng 4582

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 2741	. 2 ⊢ (𝑥 = 𝐴 → (𝑥 = 𝐵 ↔ 𝐴 = 𝐵))
2		df-sn 4569	. 2 ⊢ {𝐵} = {𝑥 ∣ 𝑥 = 𝐵}
3	1, 2	elab2g 3624	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {csn 4568

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-sn 4569

This theorem is referenced by:  elsn  4583  elsni  4585  snidg  4605  elunsn  4628  eltpg  4631  el7g  4635  eldifsn  4730  sneqrg  4783  elsucg  6388  ltxr  13060  elfzp12  13551  fzdif1  13553  fprodn0f  15950  lcmfunsnlem2  16603  ramcl  16994  initoeu2lem1  17975  pmtrdifellem4  19448  psdmul  22145  logbmpt  26768  2lgslem2  27375  xrge0tsmsbi  33153  rprmnz  33598  dimkerim  33790  elzrhunit  34140  esumrnmpt2  34231  plymulx  34711  bj-projval  37322  bj-elsn12g  37386  bj-elsnb  37387  bj-snmoore  37444  bj-elsn0  37488  eldmressnALTV  38617  brressn  38869  zndvdchrrhm  42429  aks4d1p6  42537  aks6d1c2lem4  42583  sticksstones11  42612  aks6d1c6lem2  42627  aks6d1c7lem1  42636  rhmqusspan  42641  unitscyglem2  42652  reclimc  46102  itgsincmulx  46423  dirkercncflem2  46553  dirkercncflem4  46555  fourierdlem53  46608  fourierdlem58  46613  fourierdlem60  46615  fourierdlem61  46616  fourierdlem62  46617  fourierdlem76  46631  fourierdlem101  46656  elaa2  46683  etransc  46732  qndenserrnbl  46744  sge0tsms  46829  el1fzopredsuc  47789  elclnbgrelnbgr  48316  clnbupgrel  48325  mndtcob  50072