Theorem elsn 4568

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

Hypothesis

Ref	Expression
elsn.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
elsn	⊢ (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)

Proof of Theorem elsn

Step	Hyp	Ref	Expression
1		elsn.1	. 2 ⊢ 𝐴 ∈ V
2		elsng 4567	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)

Syntax hints:   ↔ wb 208   = wceq 1537   ∈ wcel 2114  Vcvv 3486  {csn 4553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-sn 4554

This theorem is referenced by:  velsn  4569  opthwiener  5390  opthprc  5602  dmsnn0  6050  dmsnopg  6056  cnvcnvsn  6062  snsn0non  6295  funconstss  6812  fniniseg  6816  fniniseg2  6818  fsn  6883  fconstfv  6961  eusvobj2  7135  fnse  7813  wfrlem14  7954  fisn  8877  axdc3lem4  9861  axdc4lem  9863  axcclem  9865  opelreal  10538  seqid3  13404  seqz  13408  1exp  13448  hashf1lem2  13804  fprodn0f  15330  imasaddfnlem  16784  initoid  17248  termoid  17249  0subm  17965  smndex1mgm  18055  smndex1n0mnd  18060  grpinvfval  18125  0subg  18287  0nsg  18304  sylow2alem2  18726  gsumval3  19010  gsumzaddlem  19024  kerf1ghm  19480  kerf1hrmOLD  19481  lsssn0  19702  r0cld  22329  alexsubALTlem2  22639  tgphaus  22708  isusp  22853  i1f1lem  24273  ig1pcl  24755  plyco0  24768  plyeq0lem  24786  plycj  24853  wilthlem2  25632  dchrfi  25817  snstriedgval  26809  incistruhgr  26850  1loopgrnb0  27270  umgr2v2enb1  27294  usgr2pthlem  27530  hsn0elch  29009  h1de2ctlem  29316  atomli  30143  brsnop  30415  1stpreimas  30427  gsummpt2d  30694  kerunit  30903  qqhval2lem  31229  qqhf  31234  qqhre  31268  esum2dlem  31358  eulerpartlemb  31633  bnj149  32154  subfacp1lem6  32439  ellimits  33378  bj-0nel1  34281  bj-isrvec  34591  poimirlem18  34944  poimirlem21  34947  poimirlem22  34948  poimirlem31  34957  poimirlem32  34958  itg2addnclem2  34978  ftc1anclem3  35001  0idl  35335  keridl  35342  smprngopr  35362  isdmn3  35384  ellkr  36257  diblss  38338  dihmeetlem4preN  38474  dihmeetlem13N  38487  0prjspnrel  39361  pw2f1ocnv  39726  fvnonrel  40047  snhesn  40222  unirnmapsn  41567  sge0fodjrnlem  42788  lindslinindsimp1  44597