Theorem elsni 3723

Description: There is only one element in a singleton. (Contributed by NM, 5-Jun-1994.)

Assertion

Ref	Expression
elsni	⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)

Proof of Theorem elsni

Step	Hyp	Ref	Expression
1		elsng 3720	. 2 ⊢ (𝐴 ∈ {𝐵} → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
2	1	ibi 176	1 ⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)

Syntax hints:   → wi 4   = wceq 1402   ∈ wcel 2209  {csn 3705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-sn 3711

This theorem is referenced by:  elsn2g  3738  nelsn  3740  disjsn2  3768  rabsnifsb  3773  rabsnif  3774  sssnm  3874  disjxsn  4123  pwntru  4331  opth1  4371  elsuci  4543  ordtri2orexmid  4665  onsucsssucexmid  4669  sosng  4843  elrelimasn  5148  ressn  5323  funcnvsn  5421  funinsn  5425  funopdmsn  5886  fvconst  5894  fmptap  5896  fmptapd  5897  fvunsng  5900  mposnif  6172  1stconst  6447  2ndconst  6448  reldmtpos  6514  tpostpos  6525  1domsn  7105  ac6sfi  7192  elssdc  7199  onunsnss  7214  snon0  7239  snexxph  7257  elfi2  7296  supsnti  7335  djuf1olem  7383  eldju2ndl  7402  eldju2ndr  7403  difinfsnlem  7429  pw1m  7573  pw1on  7575  elreal2  8187  ax1rid  8234  ltxrlt  8381  un0addcl  9575  un0mulcl  9576  fzodisjsn  10569  elfzonlteqm1  10606  xnn0nnen  10852  fxnn0nninf  10854  seqf1og  10936  1exp  10983  hashinfuni  11194  hashennnuni  11196  hashprg  11227  zfz1isolemiso  11269  cats1un  11471  fisumss  12137  sumsnf  12154  fsumsplitsn  12155  fsum2dlemstep  12179  fisumcom2  12183  fprodssdc  12335  fprodunsn  12349  fprod2dlemstep  12367  fprodcom2fi  12371  fprodsplitsn  12378  divalgmod  12672  phi1  12975  dfphi2  12976  nnnn0modprm0  13012  exmidunben  13295  bassetsnn  13387  gzsumress  13689  0nsg  13994  gzsumsnfd  14124  gsumsncmn  14133  lsssn0  14679  lspsneq0  14735  gsumfsum  14895  txdis1cn  15302  plyaddlem1  15771  plymullem1  15772  plycoeid3  15781  plycj  15785  pw0ss  16238  usgr1vr  16403  bj-nntrans  16891  bj-nnelirr  16893  pwtrufal  16941  sssneq  16946  exmidsbthrlem  16972