Theorem elsni 4597

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  {csn 4580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-sn 4581

This theorem is referenced by:  elsnd  4598  elsn2g  4621  nelsn  4623  elpwunsn  4641  eqoreldif  4642  disjsn2  4669  rabsnifsb  4679  sssn  4782  disjxsn  5092  opth1  5423  sosn  5711  ressn  6243  elsnxp  6249  elsuci  6386  funcnvsn  6542  funopdmsn  7095  fvconst  7108  fnsnr  7109  fmptap  7116  mposnif  7474  resf1extb  7876  1stconst  8042  2ndconst  8043  reldmtpos  8176  tpostpos  8188  disjen  9062  map2xp  9075  en1eqsn  9175  ac6sfi  9184  ixpfi2  9250  elfi2  9317  fisn  9330  unxpwdom2  9493  cantnfp1lem3  9589  djulf1o  9824  djurf1o  9825  djur  9831  eldju2ndl  9836  eldju2ndr  9837  isfin4p1  10225  dcomex  10357  iundom2g  10450  fpwwe2lem12  10553  canthp1lem2  10564  0tsk  10666  elreal2  11043  ax1rid  11072  ltxrlt  11203  un0addcl  12434  un0mulcl  12435  fzodisjsn  13613  elfzonlteqm1  13657  elfzo0l  13672  elfzr  13697  elfzlmr  13698  seqf1o  13966  seqid3  13969  seqz  13973  1exp  14014  hashnn0pnf  14265  hash1elsn  14294  hashprg  14318  cats1un  14644  fsumss  15648  sumsnf  15666  fsumsplitsn  15667  fsum2dlem  15693  fsumcom2  15697  ackbijnn  15751  fprodss  15871  fprod2dlem  15903  fprodcom2  15907  fprodsplitsn  15912  sumeven  16314  sumodd  16315  divalgmod  16333  lcmfunsnlem2lem1  16565  lcmfunsnlem2lem2  16566  phi1  16700  dfphi2  16701  nnnn0modprm0  16734  ramubcl  16946  0ram  16948  ramz  16953  imasvscafn  17458  mreexmrid  17566  2initoinv  17934  2termoinv  17941  gsumress  18607  gsumval2  18611  smndex1basss  18830  smndex1mndlem  18834  0nsg  19098  symgextf1lem  19349  symgextf1  19350  pmtrprfval  19416  psgnsn  19449  lsmdisj2  19611  subgdisj1  19620  lt6abl  19824  gsumsnfd  19880  gsumzunsnd  19885  gsumunsnfd  19886  gsum2dlem2  19900  dprdfeq0  19953  dprdsn  19967  dprd2da  19973  pgpfac1lem3a  20007  pgpfaclem2  20013  ablsimpnosubgd  20035  c0snmgmhm  20398  0ring01eq  20462  zrinitorngc  20575  lsssn0  20899  lspsneq0  20963  lspdisjb  21081  pzriprnglem12  21447  frgpcyg  21528  obselocv  21683  obs2ss  21684  mplcoe5  21995  psdmul  22109  coe1tm  22215  mat0dim0  22411  mat0dimid  22412  mat0dimscm  22413  mat1dimscm  22419  mavmul0g  22497  mdet0pr  22536  mdetunilem9  22564  cramer0  22634  pmatcollpw3fi1lem1  22730  basdif0  22897  ordtbas  23136  ordtrest2  23148  cmpfi  23352  refun0  23459  txdis1cn  23579  ptrescn  23583  txkgen  23596  xkoptsub  23598  ordthmeolem  23745  pt1hmeo  23750  filconn  23827  filufint  23864  flimclslem  23928  ptcmplem3  23998  idnghm  24687  iccpnfcnv  24898  iccpnfhmeo  24899  bndth  24913  ivthicc  25415  ovoliunlem1  25459  i1fima2sn  25637  i1f1  25647  itg1addlem4  25656  itg1addlem5  25657  i1fmulc  25660  limcres  25843  limccnp  25848  limccnp2  25849  degltlem1  26033  ply1rem  26127  fta1blem  26132  ig1pdvds  26141  plyeq0lem  26171  plypf1  26173  plyaddlem1  26174  plymullem1  26175  coemulhi  26215  plycj  26239  plycjOLD  26241  taylfval  26322  abelthlem3  26399  rlimcnp  26931  wilthlem2  27035  logexprlim  27192  2sqreultblem  27415  tgldim0eq  28575  edglnl  29216  nbgr1vtx  29431  vtxdginducedm1lem4  29616  clwlkclwwlklem2a4  30072  eucrct2eupth  30320  frgrncvvdeqlem9  30382  nsnlplig  30556  nsnlpligALT  30557  fsumiunle  32910  cshw1s2  33042  gsumhashmul  33150  xrge0tsmsbi  33156  gsumwrd2dccatlem  33159  cyc3evpm  33232  0ringcring  33334  pidlnz  33457  elrspunidl  33509  0ringprmidl  33530  drngmxidlr  33559  ig1pmindeg  33683  mplmulmvr  33704  vieta  33736  lbslsat  33773  lindsunlem  33781  irngnminplynz  33869  ordtrest2NEW  34080  xrge0iifcnv  34090  xrge0iifhom  34094  esumsnf  34221  esumpr  34223  esumiun  34251  inelpisys  34311  measvunilem0  34370  measvuni  34371  carsggect  34475  omsmeas  34480  plymulx0  34704  repr0  34768  bnj98  35023  bnj1442  35205  bnj1452  35208  subfacp1lem5  35378  erdszelem4  35388  erdszelem8  35392  sconnpi1  35433  cvmlift2lem6  35502  cvmlift2lem12  35508  fmla0xp  35577  onint1  36643  bj-1nel0  37155  bj-sngltag  37184  bj-projval  37197  bj-elsn0  37360  bj-fununsn1  37458  tan2h  37813  lindsenlbs  37816  matunitlindf  37819  ptrest  37820  poimirlem23  37844  poimirlem24  37845  poimirlem25  37846  poimirlem28  37849  poimirlem29  37850  poimirlem30  37851  poimirlem31  37852  poimirlem32  37853  prdsbnd  37994  rrnequiv  38036  grpokerinj  38094  rngoueqz  38141  gidsn  38153  0rngo  38228  isdmn3  38275  dibelval2nd  41412  hdmaprnlem9N  42117  hdmap14lem4a  42131  dvrelog2b  42320  sticksstones11  42410  unitscyglem2  42450  0prjspnrel  42870  hbtlem5  43370  flcidc  43412  safesnsupfiss  43656  frege133d  44006  radcnvrat  44555  unisnALT  45166  sumsnd  45271  fnchoice  45274  rnsnf  45428  founiiun0  45434  elmapsnd  45448  fsneqrn  45455  infxrpnf  45690  supminfxr2  45713  cncfiooicc  46138  fperdvper  46163  dvmptfprodlem  46188  dvnprodlem1  46190  dvnprodlem2  46191  itgcoscmulx  46213  stoweidlem44  46288  fourierdlem49  46399  fourierdlem56  46406  fourierdlem80  46430  fourierdlem93  46443  fourierdlem101  46451  sge00  46620  sge0sn  46623  sge0snmpt  46627  sge0iunmptlemfi  46657  sge0p1  46658  sge0fodjrnlem  46660  sge0snmptf  46681  sge0splitsn  46685  nnfoctbdjlem  46699  meadjiunlem  46709  ismeannd  46711  caratheodorylem1  46770  isomenndlem  46774  hoidmv1le  46838  hoidmvlelem2  46840  hoidmvlelem3  46841  ovnhoilem1  46845  hoiqssbl  46869  ovnovollem1  46900  ovnovollem2  46901  chnerlem1  47126  eldmressn  47283  iccpartltu  47671  sbgoldbo  48033  nnsum3primesprm  48036  bgoldbtbndlem3  48053  stgr1  48207  gpgprismgr4cycllem7  48347  ldepspr  48719  lmod1zr  48739  termcbas2  49727  idfudiag1  49770