Theorem elsnc 3757

Description: There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. (Contributed by NM, 13-Sep-1995.)

Hypothesis

Ref	Expression
elsnc.1	⊢ A ∈ V

Assertion

Ref	Expression
elsnc	⊢ (A ∈ {B} ↔ A = B)

Proof of Theorem elsnc

Step	Hyp	Ref	Expression
1		elsnc.1	. 2 ⊢ A ∈ V
2		elsncg 3756	. 2 ⊢ (A ∈ V → (A ∈ {B} ↔ A = B))
3	1, 2	ax-mp 5	1 ⊢ (A ∈ {B} ↔ A = B)

Syntax hints:   ↔ wb 176   = wceq 1642   ∈ wcel 1710  Vcvv 2860  {csn 3738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-v 2862  df-sn 3742

This theorem is referenced by:  sneqr  3873  sniota  4370  nnsucelrlem1  4425  nnsucelrlem3  4427  nnsucelr  4429  nndisjeq  4430  ltfinex  4465  ltfintrilem1  4466  ssfin  4471  eqtfinrelk  4487  oddfinex  4505  evenoddnnnul  4515  evenodddisjlem1  4516  nnadjoinlem1  4520  vfinspss  4552  dfop2lem1  4574  setconslem2  4733  dmsnn0  5065  dmsnopg  5067  cnvsn  5074  rnsnop  5076  funsn  5148  iunfopab  5205  funconstss  5407  fsn  5433  fvclss  5463  1p1e2c  6156  fce  6189  dmfrec  6317