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  7346  djuf1olem  7394  eldju2ndl  7413  eldju2ndr  7414  difinfsnlem  7440  pw1m  7584  pw1on  7586  elreal2  8198  ax1rid  8245  ltxrlt  8392  un0addcl  9601  un0mulcl  9602  fzodisjsn  10602  elfzonlteqm1  10639  xnn0nnen  10889  fxnn0nninf  10891  seqf1og  10973  1exp  11020  hashinfuni  11232  hashennnuni  11234  hashprg  11265  zfz1isolemiso  11307  cats1un  11509  fisumss  12178  sumsnf  12195  fsumsplitsn  12196  fsum2dlemstep  12220  fisumcom2  12224  fprodssdc  12376  fprodunsn  12390  fprod2dlemstep  12408  fprodcom2fi  12412  fprodsplitsn  12419  divalgmod  12713  phi1  13020  dfphi2  13021  nnnn0modprm0  13057  exmidunben  13369  bassetsnn  13461  gzsumress  13765  0nsg  14070  gzsumsnfd  14231  gsumsncmn  14240  lsssn0  14791  lspsneq0  14847  gsumfsum  15007  txdis1cn  15470  plyaddlem1  15939  plymullem1  15940  plycoeid3  15949  plycj  15953  pw0ss  16490  usgr1vr  16655  bj-nntrans  17143  bj-nnelirr  17145  pwtrufal  17193  sssneq  17198  wexmiddifxylem  17211  exmidsbthrlem  17233