Theorem elsng 4645

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∈ wcel 2106  {csn 4631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-sn 4632

This theorem is referenced by:  elsn  4646  elsni  4648  snidg  4665  elunsn  4688  eltpg  4691  el7g  4695  eldifsn  4791  sneqrg  4844  elsucg  6454  ltxr  13155  elfzp12  13640  fzdif1  13642  fprodn0f  16024  lcmfunsnlem2  16674  ramcl  17063  initoeu2lem1  18068  pmtrdifellem4  19512  psdmul  22188  logbmpt  26846  2lgslem2  27454  xrge0tsmsbi  33049  rprmnz  33528  dimkerim  33655  elzrhunit  33940  esumrnmpt2  34049  plymulx  34542  bj-projval  36979  bj-elsn12g  37043  bj-elsnb  37044  bj-snmoore  37096  bj-elsn0  37138  eldmressnALTV  38254  brressn  38423  zndvdchrrhm  41953  aks4d1p6  42063  aks6d1c2lem4  42109  sticksstones11  42138  aks6d1c6lem2  42153  aks6d1c7lem1  42162  rhmqusspan  42167  unitscyglem2  42178  metakunt20  42206  reclimc  45609  itgsincmulx  45930  dirkercncflem2  46060  dirkercncflem4  46062  fourierdlem53  46115  fourierdlem58  46120  fourierdlem60  46122  fourierdlem61  46123  fourierdlem62  46124  fourierdlem76  46138  fourierdlem101  46163  elaa2  46190  etransc  46239  qndenserrnbl  46251  sge0tsms  46336  el1fzopredsuc  47275  elclnbgrelnbgr  47750  clnbupgrel  47759  mndtcob  48891