Theorem elsnc 2427

Description: There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15.

Hypothesis

Ref	Expression
elsnc.1	|- A e. V

Assertion

Ref	Expression
elsnc	|- (A e. {B} <-> A = B)

Proof of Theorem elsnc

Step	Hyp	Ref	Expression
1		elsnc.1	. 2 |- A e. V
2		elsncg 2426	. 2 |- (A e. V -> (A e. {B} <-> A = B))
3	1, 2	ax-mp 7	1 |- (A e. {B} <-> A = B)

Syntax hints:   <-> wb 146   = wceq 954   e. wcel 956  Vcvv 1807  {csn 2405

This theorem is referenced by:  eltp 2435  sneqr 2473  opth1 2781  opthwiener 2802  snsn0non 3120  opthprc 3216  dmsn0 3319  dmsnsn0 3320  dmsnop 3323  cnvsn 3441  funsn 3535  funconstss 3799  fsn 3825  1st2val 4085  2nd2val 4086  opelreal 5229  ltxrt 5475  sn0top 7597  hsn0elch 9059  h1de2ctlem 9417  atoml 10246  oefil2 10477

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-un 2046  df-sn 2408  df-pr 2409

Copyright terms: Public domain