Theorem elsni 3594

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 3591	. 2 ⊢ (𝐴 ∈ {𝐵} → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
2	1	ibi 175	1 ⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)

Syntax hints:   → wi 4   = wceq 1343   ∈ wcel 2136  {csn 3576

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-v 2728  df-sn 3582

This theorem is referenced by:  elsn2g  3609  nelsn  3611  disjsn2  3639  sssnm  3734  disjxsn  3980  pwntru  4178  opth1  4214  elsuci  4381  ordtri2orexmid  4500  onsucsssucexmid  4504  sosng  4677  ressn  5144  funcnvsn  5233  funinsn  5237  fvconst  5673  fmptap  5675  fmptapd  5676  fvunsng  5679  mposnif  5936  1stconst  6189  2ndconst  6190  reldmtpos  6221  tpostpos  6232  1domsn  6785  ac6sfi  6864  onunsnss  6882  snon0  6901  snexxph  6915  elfi2  6937  supsnti  6970  djuf1olem  7018  eldju2ndl  7037  eldju2ndr  7038  difinfsnlem  7064  pw1on  7182  elreal2  7771  ax1rid  7818  ltxrlt  7964  un0addcl  9147  un0mulcl  9148  elfzonlteqm1  10145  fxnn0nninf  10373  1exp  10484  hashinfuni  10690  hashennnuni  10692  hashprg  10721  zfz1isolemiso  10752  fisumss  11333  sumsnf  11350  fsumsplitsn  11351  fsum2dlemstep  11375  fisumcom2  11379  fprodssdc  11531  fprodunsn  11545  fprod2dlemstep  11563  fprodcom2fi  11567  fprodsplitsn  11574  divalgmod  11864  phi1  12151  dfphi2  12152  nnnn0modprm0  12187  exmidunben  12359  txdis1cn  12918  bj-nntrans  13833  bj-nnelirr  13835  pwtrufal  13877  sssneq  13882  exmidsbthrlem  13901