Theorem elsni 3612

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

Syntax hints:   → wi 4   = wceq 1353   ∈ wcel 2148  {csn 3594

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2741  df-sn 3600

This theorem is referenced by:  elsn2g  3627  nelsn  3629  disjsn2  3657  sssnm  3756  disjxsn  4003  pwntru  4201  opth1  4238  elsuci  4405  ordtri2orexmid  4524  onsucsssucexmid  4528  sosng  4701  elrelimasn  4996  ressn  5171  funcnvsn  5263  funinsn  5267  fvconst  5706  fmptap  5708  fmptapd  5709  fvunsng  5712  mposnif  5971  1stconst  6224  2ndconst  6225  reldmtpos  6256  tpostpos  6267  1domsn  6821  ac6sfi  6900  onunsnss  6918  snon0  6937  snexxph  6951  elfi2  6973  supsnti  7006  djuf1olem  7054  eldju2ndl  7073  eldju2ndr  7074  difinfsnlem  7100  pw1on  7227  elreal2  7831  ax1rid  7878  ltxrlt  8025  un0addcl  9211  un0mulcl  9212  elfzonlteqm1  10212  fxnn0nninf  10440  1exp  10551  hashinfuni  10759  hashennnuni  10761  hashprg  10790  zfz1isolemiso  10821  fisumss  11402  sumsnf  11419  fsumsplitsn  11420  fsum2dlemstep  11444  fisumcom2  11448  fprodssdc  11600  fprodunsn  11614  fprod2dlemstep  11632  fprodcom2fi  11636  fprodsplitsn  11643  divalgmod  11934  phi1  12221  dfphi2  12222  nnnn0modprm0  12257  exmidunben  12429  0nsg  13079  lsssn0  13462  lspsneq0  13517  txdis1cn  13863  bj-nntrans  14788  bj-nnelirr  14790  pwtrufal  14832  sssneq  14836  exmidsbthrlem  14855