Theorem elsni 3651

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

Syntax hints:   → wi 4   = wceq 1373   ∈ wcel 2176  {csn 3633

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-sn 3639

This theorem is referenced by:  elsn2g  3666  nelsn  3668  disjsn2  3696  sssnm  3795  disjxsn  4042  pwntru  4243  opth1  4280  elsuci  4450  ordtri2orexmid  4571  onsucsssucexmid  4575  sosng  4748  elrelimasn  5048  ressn  5223  funcnvsn  5319  funinsn  5323  funopdmsn  5764  fvconst  5772  fmptap  5774  fmptapd  5775  fvunsng  5778  mposnif  6039  1stconst  6307  2ndconst  6308  reldmtpos  6339  tpostpos  6350  1domsn  6914  ac6sfi  6995  onunsnss  7014  snon0  7037  snexxph  7052  elfi2  7074  supsnti  7107  djuf1olem  7155  eldju2ndl  7174  eldju2ndr  7175  difinfsnlem  7201  pw1on  7338  elreal2  7943  ax1rid  7990  ltxrlt  8138  un0addcl  9328  un0mulcl  9329  elfzonlteqm1  10339  xnn0nnen  10582  fxnn0nninf  10584  seqf1og  10666  1exp  10713  hashinfuni  10922  hashennnuni  10924  hashprg  10953  zfz1isolemiso  10984  fisumss  11703  sumsnf  11720  fsumsplitsn  11721  fsum2dlemstep  11745  fisumcom2  11749  fprodssdc  11901  fprodunsn  11915  fprod2dlemstep  11933  fprodcom2fi  11937  fprodsplitsn  11944  divalgmod  12238  phi1  12541  dfphi2  12542  nnnn0modprm0  12578  exmidunben  12797  gsumress  13227  0nsg  13550  gsumfzsnfd  13681  lsssn0  14132  lspsneq0  14188  txdis1cn  14750  plyaddlem1  15219  plymullem1  15220  plycoeid3  15229  plycj  15233  bj-nntrans  15887  bj-nnelirr  15889  pwtrufal  15934  sssneq  15939  exmidsbthrlem  15961