Theorem elsni 3685

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

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200  {csn 3667

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2802  df-sn 3673

This theorem is referenced by:  elsn2g  3700  nelsn  3702  disjsn2  3730  rabsnifsb  3735  rabsnif  3736  sssnm  3835  disjxsn  4084  pwntru  4287  opth1  4326  elsuci  4498  ordtri2orexmid  4619  onsucsssucexmid  4623  sosng  4797  elrelimasn  5100  ressn  5275  funcnvsn  5372  funinsn  5376  funopdmsn  5829  fvconst  5837  fmptap  5839  fmptapd  5840  fvunsng  5843  mposnif  6110  1stconst  6381  2ndconst  6382  reldmtpos  6414  tpostpos  6425  1domsn  6996  ac6sfi  7080  elssdc  7087  onunsnss  7102  snon0  7125  snexxph  7140  elfi2  7162  supsnti  7195  djuf1olem  7243  eldju2ndl  7262  eldju2ndr  7263  difinfsnlem  7289  pw1m  7432  pw1on  7434  elreal2  8040  ax1rid  8087  ltxrlt  8235  un0addcl  9425  un0mulcl  9426  fzodisjsn  10409  elfzonlteqm1  10445  xnn0nnen  10689  fxnn0nninf  10691  seqf1og  10773  1exp  10820  hashinfuni  11029  hashennnuni  11031  hashprg  11062  zfz1isolemiso  11093  cats1un  11292  fisumss  11943  sumsnf  11960  fsumsplitsn  11961  fsum2dlemstep  11985  fisumcom2  11989  fprodssdc  12141  fprodunsn  12155  fprod2dlemstep  12173  fprodcom2fi  12177  fprodsplitsn  12184  divalgmod  12478  phi1  12781  dfphi2  12782  nnnn0modprm0  12818  exmidunben  13037  bassetsnn  13129  gsumress  13468  0nsg  13791  gsumfzsnfd  13922  lsssn0  14374  lspsneq0  14430  txdis1cn  14992  plyaddlem1  15461  plymullem1  15462  plycoeid3  15471  plycj  15475  pw0ss  15924  usgr1vr  16087  bj-nntrans  16482  bj-nnelirr  16484  pwtrufal  16534  sssneq  16539  exmidsbthrlem  16562