Theorem elsni 4579

Description: There is at most 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 4576	. 2 ⊢ (𝐴 ∈ {𝐵} → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
2	1	ibi 266	1 ⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  {csn 4562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-sn 4563

This theorem is referenced by:  elsn2g  4600  nelsn  4602  elpwunsn  4620  eqoreldif  4621  disjsn2  4649  rabsnifsb  4659  sssn  4760  disjxsn  5068  opth1  5391  sosn  5674  ressn  6192  elsnxp  6198  elsuci  6336  funcnvsn  6491  funopdmsn  7031  fvconst  7045  fnsnr  7046  fmptap  7051  mposnif  7399  1stconst  7949  2ndconst  7950  reldmtpos  8059  tpostpos  8071  disjen  8930  map2xp  8943  ac6sfi  9067  ixpfi2  9126  elfi2  9182  fisn  9195  unxpwdom2  9356  cantnfp1lem3  9447  djulf1o  9679  djurf1o  9680  djur  9686  eldju2ndl  9691  eldju2ndr  9692  isfin4p1  10080  dcomex  10212  iundom2g  10305  fpwwe2lem12  10407  canthp1lem2  10418  0tsk  10520  elreal2  10897  ax1rid  10926  ltxrlt  11054  un0addcl  12275  un0mulcl  12276  fzodisjsn  13434  elfzonlteqm1  13472  elfzo0l  13486  elfzr  13509  elfzlmr  13510  seqf1o  13773  seqid3  13776  seqz  13780  1exp  13821  hashnn0pnf  14065  hash1elsn  14095  hashprg  14119  cats1un  14443  fsumss  15446  sumsnf  15464  fsumsplitsn  15465  fsum2dlem  15491  fsumcom2  15495  ackbijnn  15549  fprodss  15667  fprod2dlem  15699  fprodcom2  15703  fprodsplitsn  15708  sumeven  16105  sumodd  16106  divalgmod  16124  lcmfunsnlem2lem1  16352  lcmfunsnlem2lem2  16353  phi1  16483  dfphi2  16484  nnnn0modprm0  16516  ramubcl  16728  0ram  16730  ramz  16735  imasvscafn  17257  mreexmrid  17361  2initoinv  17734  2termoinv  17741  gsumress  18375  gsumval2  18379  smndex1basss  18553  smndex1mndlem  18557  0nsg  18806  symgextf1lem  19037  symgextf1  19038  pmtrprfval  19104  psgnsn  19137  lsmdisj2  19297  subgdisj1  19306  lt6abl  19505  gsumsnfd  19561  gsumzunsnd  19566  gsumunsnfd  19567  gsum2dlem2  19581  dprdfeq0  19634  dprdsn  19648  dprd2da  19654  pgpfac1lem3a  19688  pgpfaclem2  19694  ablsimpnosubgd  19716  lsssn0  20218  lspsneq0  20283  lspdisjb  20397  0ring01eq  20551  frgpcyg  20790  obselocv  20944  obs2ss  20945  mplcoe5  21250  coe1tm  21453  mat0dim0  21625  mat0dimid  21626  mat0dimscm  21627  mat1dimscm  21633  mavmul0g  21711  mdet0pr  21750  mdetunilem9  21778  cramer0  21848  pmatcollpw3fi1lem1  21944  basdif0  22112  ordtbas  22352  ordtrest2  22364  cmpfi  22568  refun0  22675  txdis1cn  22795  ptrescn  22799  txkgen  22812  xkoptsub  22814  ordthmeolem  22961  pt1hmeo  22966  filconn  23043  filufint  23080  flimclslem  23144  ptcmplem3  23214  idnghm  23916  iccpnfcnv  24116  iccpnfhmeo  24117  bndth  24130  ivthicc  24631  ovoliunlem1  24675  i1fima2sn  24853  i1f1  24863  itg1addlem4  24872  itg1addlem4OLD  24873  itg1addlem5  24874  i1fmulc  24877  limcres  25059  limccnp  25064  limccnp2  25065  degltlem1  25246  ply1rem  25337  fta1blem  25342  ig1pdvds  25350  plyeq0lem  25380  plypf1  25382  plyaddlem1  25383  plymullem1  25384  coemulhi  25424  plycj  25447  taylfval  25527  abelthlem3  25601  rlimcnp  26124  wilthlem2  26227  logexprlim  26382  2sqreultblem  26605  tgldim0eq  26873  edglnl  27522  nbgr1vtx  27734  vtxdginducedm1lem4  27918  clwlkclwwlklem2a4  28370  eucrct2eupth  28618  frgrncvvdeqlem9  28680  nsnlplig  28852  nsnlpligALT  28853  fsumiunle  31152  cshw1s2  31241  gsumhashmul  31325  xrge0tsmsbi  31327  cyc3evpm  31426  pidlnz  31580  elrspunidl  31615  0ringprmidl  31634  lbslsat  31708  lindsunlem  31714  ordtrest2NEW  31882  xrge0iifcnv  31892  xrge0iifhom  31896  esumsnf  32041  esumpr  32043  esumiun  32071  inelpisys  32131  measvunilem0  32190  measvuni  32191  carsggect  32294  omsmeas  32299  plymulx0  32535  repr0  32600  bnj98  32856  bnj1442  33038  bnj1452  33041  subfacp1lem5  33155  erdszelem4  33165  erdszelem8  33169  sconnpi1  33210  cvmlift2lem6  33279  cvmlift2lem12  33285  fmla0xp  33354  onint1  34647  bj-1nel0  35153  bj-sngltag  35182  bj-projval  35195  bj-elsn0  35335  bj-fununsn1  35433  tan2h  35778  lindsenlbs  35781  matunitlindf  35784  ptrest  35785  poimirlem23  35809  poimirlem24  35810  poimirlem25  35811  poimirlem28  35814  poimirlem29  35815  poimirlem30  35816  poimirlem31  35817  poimirlem32  35818  prdsbnd  35960  rrnequiv  36002  grpokerinj  36060  rngoueqz  36107  gidsn  36119  0rngo  36194  isdmn3  36241  dibelval2nd  39173  hdmaprnlem9N  39878  hdmap14lem4a  39892  dvrelog2b  40081  sticksstones11  40119  0prjspnrel  40471  hbtlem5  40960  flcidc  41006  frege133d  41380  radcnvrat  41939  unisnALT  42553  sumsnd  42576  fnchoice  42579  rnsnf  42728  founiiun0  42735  elmapsnd  42751  fsneqrn  42758  infxrpnf  42993  supminfxr2  43016  cncfiooicc  43442  fperdvper  43467  dvmptfprodlem  43492  dvnprodlem1  43494  dvnprodlem2  43495  itgcoscmulx  43517  stoweidlem44  43592  fourierdlem49  43703  fourierdlem56  43710  fourierdlem80  43734  fourierdlem93  43747  fourierdlem101  43755  sge00  43921  sge0sn  43924  sge0snmpt  43928  sge0iunmptlemfi  43958  sge0p1  43959  sge0fodjrnlem  43961  sge0snmptf  43982  sge0splitsn  43986  nnfoctbdjlem  44000  meadjiunlem  44010  ismeannd  44012  caratheodorylem1  44071  isomenndlem  44075  hoidmv1le  44139  hoidmvlelem2  44141  hoidmvlelem3  44142  ovnhoilem1  44146  hoiqssbl  44170  ovnovollem1  44201  ovnovollem2  44202  eldmressn  44542  iccpartltu  44888  sbgoldbo  45250  nnsum3primesprm  45253  bgoldbtbndlem3  45270  c0snmgmhm  45483  zrinitorngc  45569  ldepspr  45825  lmod1zr  45845