Theorem elsni 3727

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209  {csn 3709

This proof depends on 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 proof 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 3715

This theorem is used by:  elsn2g  3742  nelsn  3744  disjsn2  3772  rabsnifsb  3777  rabsnif  3778  sssnm  3879  disjxsn  4128  pwntru  4336  opth1  4376  elsuci  4548  ordtri2orexmid  4670  onsucsssucexmid  4674  sosng  4848  elrelimasn  5153  ressn  5328  funcnvsn  5426  funinsn  5430  funopdmsn  5895  fvconst  5903  fmptap  5905  fmptapd  5906  fvunsng  5909  mposnif  6182  1stconst  6457  2ndconst  6458  reldmtpos  6524  tpostpos  6535  1domsn  7115  ac6sfi  7202  elssdc  7209  onunsnss  7224  snon0  7249  snexxph  7267  elfi2  7306  supsnti  7345  djuf1olem  7393  eldju2ndl  7412  eldju2ndr  7413  difinfsnlem  7439  pw1m  7583  pw1on  7585  elreal2  8197  ax1rid  8244  ltxrlt  8391  un0addcl  9600  un0mulcl  9601  fzodisjsn  10601  elfzonlteqm1  10638  xnn0nnen  10887  fxnn0nninf  10889  seqf1og  10971  1exp  11018  hashinfuni  11230  hashennnuni  11232  hashprg  11263  zfz1isolemiso  11305  cats1un  11507  fisumss  12175  sumsnf  12192  fsumsplitsn  12193  fsum2dlemstep  12217  fisumcom2  12221  fprodssdc  12373  fprodunsn  12387  fprod2dlemstep  12405  fprodcom2fi  12409  fprodsplitsn  12416  divalgmod  12710  phi1  13017  dfphi2  13018  nnnn0modprm0  13054  exmidunben  13366  bassetsnn  13458  gzsumress  13761  0nsg  14066  gzsumsnfd  14196  gsumsncmn  14205  lsssn0  14756  lspsneq0  14812  gsumfsum  14972  txdis1cn  15428  plyaddlem1  15897  plymullem1  15898  plycoeid3  15907  plycj  15911  pw0ss  16422  usgr1vr  16587  bj-nntrans  17075  bj-nnelirr  17077  pwtrufal  17125  sssneq  17130  wexmiddifxylem  17143  exmidsbthrlem  17165