Theorem elsng 4541

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1543   ∈ wcel 2112  {csn 4527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-sn 4528

This theorem is referenced by:  elsn  4542  elsni  4544  snidg  4561  eltpg  4587  eldifsn  4686  sneqrg  4736  elsucg  6258  ltxr  12672  elfzp12  13156  fprodn0f  15516  lcmfunsnlem2  16160  ramcl  16545  initoeu2lem1  17474  pmtrdifellem4  18825  logbmpt  25625  2lgslem2  26230  elunsn  30531  xrge0tsmsbi  30991  dimkerim  31376  elzrhunit  31595  esumrnmpt2  31702  plymulx  32193  bj-projval  34872  bj-elsn12g  34917  bj-elsnb  34918  bj-snmoore  34968  bj-elsn0  35010  sticksstones11  39781  metakunt20  39807  reclimc  42812  itgsincmulx  43133  dirkercncflem2  43263  dirkercncflem4  43265  fourierdlem53  43318  fourierdlem58  43323  fourierdlem60  43325  fourierdlem61  43326  fourierdlem62  43327  fourierdlem76  43341  fourierdlem101  43366  elaa2  43393  etransc  43442  qndenserrnbl  43454  sge0tsms  43536  el1fzopredsuc  44433  mndtcob  45983