Theorem elsni 3656

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

Syntax hints:   → wi 4   = wceq 1373   ∈ wcel 2177  {csn 3638

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-sn 3644

This theorem is referenced by:  elsn2g  3671  nelsn  3673  disjsn2  3701  sssnm  3803  disjxsn  4052  pwntru  4254  opth1  4293  elsuci  4463  ordtri2orexmid  4584  onsucsssucexmid  4588  sosng  4761  elrelimasn  5062  ressn  5237  funcnvsn  5333  funinsn  5337  funopdmsn  5782  fvconst  5790  fmptap  5792  fmptapd  5793  fvunsng  5796  mposnif  6057  1stconst  6325  2ndconst  6326  reldmtpos  6357  tpostpos  6368  1domsn  6934  ac6sfi  7016  onunsnss  7035  snon0  7058  snexxph  7073  elfi2  7095  supsnti  7128  djuf1olem  7176  eldju2ndl  7195  eldju2ndr  7196  difinfsnlem  7222  pw1m  7365  pw1on  7367  elreal2  7973  ax1rid  8020  ltxrlt  8168  un0addcl  9358  un0mulcl  9359  fzodisjsn  10336  elfzonlteqm1  10371  xnn0nnen  10614  fxnn0nninf  10616  seqf1og  10698  1exp  10745  hashinfuni  10954  hashennnuni  10956  hashprg  10985  zfz1isolemiso  11016  cats1un  11207  fisumss  11788  sumsnf  11805  fsumsplitsn  11806  fsum2dlemstep  11830  fisumcom2  11834  fprodssdc  11986  fprodunsn  12000  fprod2dlemstep  12018  fprodcom2fi  12022  fprodsplitsn  12029  divalgmod  12323  phi1  12626  dfphi2  12627  nnnn0modprm0  12663  exmidunben  12882  gsumress  13312  0nsg  13635  gsumfzsnfd  13766  lsssn0  14217  lspsneq0  14273  txdis1cn  14835  plyaddlem1  15304  plymullem1  15305  plycoeid3  15314  plycj  15318  pw0ss  15764  bj-nntrans  16056  bj-nnelirr  16058  pwtrufal  16106  sssneq  16111  exmidsbthrlem  16133