Theorem elsni 4565

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  {csn 4548

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-sn 4549

This theorem is referenced by:  elsn2g  4584  nelsn  4586  elpwunsn  4602  eqoreldif  4603  disjsn2  4629  rabsnifsb  4639  sssn  4740  disjxsn  5040  opth1  5348  sosn  5619  ressn  6117  elsnxp  6123  elsuci  6238  funcnvsn  6385  funopdmsn  6893  fvconst  6907  fnsnr  6908  fmptap  6913  mposnif  7249  1stconst  7776  2ndconst  7777  reldmtpos  7881  tpostpos  7893  disjen  8655  map2xp  8668  ac6sfi  8743  ixpfi2  8803  elfi2  8859  fisn  8872  unxpwdom2  9033  cantnfp1lem3  9124  djulf1o  9322  djurf1o  9323  djur  9329  eldju2ndl  9334  eldju2ndr  9335  isfin4p1  9718  dcomex  9850  iundom2g  9943  fpwwe2lem13  10045  canthp1lem2  10056  0tsk  10158  elreal2  10535  ax1rid  10564  ltxrlt  10692  un0addcl  11912  un0mulcl  11913  fzodisjsn  13060  elfzonlteqm1  13098  elfzo0l  13112  elfzr  13135  elfzlmr  13136  seqf1o  13396  seqid3  13399  seqz  13403  1exp  13443  hashnn0pnf  13687  hash1elsn  13717  hashprg  13741  cats1un  14063  fsumss  15062  sumsnf  15079  fsumsplitsn  15080  fsum2dlem  15105  fsumcom2  15109  ackbijnn  15163  fprodss  15282  fprod2dlem  15314  fprodcom2  15318  fprodsplitsn  15323  sumeven  15716  sumodd  15717  divalgmod  15735  lcmfunsnlem2lem1  15960  lcmfunsnlem2lem2  15961  phi1  16088  dfphi2  16089  nnnn0modprm0  16121  ramubcl  16332  0ram  16334  ramz  16339  imasvscafn  16788  mreexmrid  16892  2initoinv  17248  2termoinv  17255  gsumress  17870  gsumval2  17874  smndex1basss  18048  smndex1mndlem  18052  0nsg  18299  symgextf1lem  18526  symgextf1  18527  pmtrprfval  18593  psgnsn  18626  lsmdisj2  18786  subgdisj1  18795  lt6abl  18993  gsumsnfd  19049  gsumzunsnd  19054  gsumunsnfd  19055  gsum2dlem2  19069  dprdfeq0  19122  dprdsn  19136  dprd2da  19142  pgpfac1lem3a  19176  pgpfaclem2  19182  ablsimpnosubgd  19204  lsssn0  19697  lspsneq0  19762  lspdisjb  19876  0ring01eq  20022  mplcoe5  20227  coe1tm  20419  frgpcyg  20698  obselocv  20850  obs2ss  20851  mat0dim0  21054  mat0dimid  21055  mat0dimscm  21056  mat1dimscm  21062  mavmul0g  21140  mdet0pr  21179  mdetunilem9  21207  cramer0  21277  pmatcollpw3fi1lem1  21372  basdif0  21539  ordtbas  21778  ordtrest2  21790  cmpfi  21994  refun0  22101  txdis1cn  22221  ptrescn  22225  txkgen  22238  xkoptsub  22240  ordthmeolem  22387  pt1hmeo  22392  filconn  22469  filufint  22506  flimclslem  22570  ptcmplem3  22640  idnghm  23330  iccpnfcnv  23526  iccpnfhmeo  23527  bndth  23540  ivthicc  24037  ovoliunlem1  24081  i1fima2sn  24259  i1f1  24269  itg1addlem4  24278  itg1addlem5  24279  i1fmulc  24282  limcres  24464  limccnp  24469  limccnp2  24470  degltlem1  24647  ply1rem  24738  fta1blem  24743  ig1pdvds  24751  plyeq0lem  24781  plypf1  24783  plyaddlem1  24784  plymullem1  24785  coemulhi  24825  plycj  24848  taylfval  24928  abelthlem3  25002  rlimcnp  25524  wilthlem2  25627  logexprlim  25782  2sqreultblem  26005  tgldim0eq  26270  edglnl  26909  nbgr1vtx  27121  vtxdginducedm1lem4  27305  clwlkclwwlklem2a4  27755  eucrct2eupth  28003  frgrncvvdeqlem9  28065  nsnlplig  28237  nsnlpligALT  28238  fsumiunle  30526  cshw1s2  30615  xrge0tsmsbi  30695  cyc3evpm  30794  pidlnz  30940  lbslsat  31019  lindsunlem  31025  ordtrest2NEW  31168  xrge0iifcnv  31178  xrge0iifhom  31182  esumsnf  31325  esumpr  31327  esumiun  31355  inelpisys  31415  measvunilem0  31474  measvuni  31475  carsggect  31578  omsmeas  31583  plymulx0  31819  repr0  31884  bnj98  32141  bnj1442  32323  bnj1452  32326  subfacp1lem5  32433  erdszelem4  32443  erdszelem8  32447  sconnpi1  32488  cvmlift2lem6  32557  cvmlift2lem12  32563  fmla0xp  32632  onint1  33799  bj-1nel0  34277  bj-sngltag  34306  bj-projval  34319  bj-elsn0  34458  bj-fununsn1  34546  bj-isrvec  34586  tan2h  34913  lindsenlbs  34916  matunitlindf  34919  ptrest  34920  poimirlem23  34944  poimirlem24  34945  poimirlem25  34946  poimirlem28  34949  poimirlem29  34950  poimirlem30  34951  poimirlem31  34952  poimirlem32  34953  prdsbnd  35098  rrnequiv  35140  grpokerinj  35198  rngoueqz  35245  gidsn  35257  0rngo  35332  isdmn3  35379  dibelval2nd  38315  hdmaprnlem9N  39020  hdmap14lem4a  39034  0prjspnrel  39356  hbtlem5  39815  flcidc  39861  frege133d  40195  radcnvrat  40731  unisnALT  41345  sumsnd  41368  fnchoice  41371  rnsnf  41529  founiiun0  41536  elmapsnd  41552  fsneqrn  41559  infxrpnf  41806  supminfxr2  41830  cncfiooicc  42262  fperdvper  42288  dvmptfprodlem  42314  dvnprodlem1  42316  dvnprodlem2  42317  itgcoscmulx  42339  stoweidlem44  42414  fourierdlem49  42525  fourierdlem56  42532  fourierdlem80  42556  fourierdlem93  42569  fourierdlem101  42577  sge00  42743  sge0sn  42746  sge0snmpt  42750  sge0iunmptlemfi  42780  sge0p1  42781  sge0fodjrnlem  42783  sge0snmptf  42804  sge0splitsn  42808  nnfoctbdjlem  42822  meadjiunlem  42832  ismeannd  42834  caratheodorylem1  42893  isomenndlem  42897  hoidmv1le  42961  hoidmvlelem2  42963  hoidmvlelem3  42964  ovnhoilem1  42968  hoiqssbl  42992  ovnovollem1  43023  ovnovollem2  43024  eldmressn  43357  iccpartltu  43670  sbgoldbo  44032  nnsum3primesprm  44035  bgoldbtbndlem3  44052  c0snmgmhm  44265  zrinitorngc  44351  ldepspr  44608  lmod1zr  44628