Theorem elsni 4194

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

Syntax hints:   → wi 4   = wceq 1483   ∈ wcel 1990  {csn 4177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-sn 4178

This theorem is referenced by:  elsn2g  4210  nelsn  4212  elpwunsn  4224  eqoreldif  4225  eqoreldifOLD  4226  disjsn2  4247  rabsnifsb  4257  sssn  4358  disjxsn  4646  opth1  4944  sosn  5188  ressn  5671  elsnxp  5677  elsuci  5791  funcnvsn  5936  funopdmsn  6415  fvconst  6431  fnsnb  6432  fmptap  6436  mpt2snif  6754  1stconst  7265  2ndconst  7266  reldmtpos  7360  tpostpos  7372  disjen  8117  map2xp  8130  ac6sfi  8204  ixpfi2  8264  elfi2  8320  fisn  8333  unxpwdom2  8493  cantnfp1lem3  8577  isfin4-3  9137  dcomex  9269  iundom2g  9362  fpwwe2lem13  9464  canthp1lem2  9475  0tsk  9577  elreal2  9953  ax1rid  9982  ltxrlt  10108  un0addcl  11326  un0mulcl  11327  fzodisjsn  12505  elfzonlteqm1  12543  elfzo0l  12558  elfzr  12581  elfzlmr  12582  seqf1o  12842  seqid3  12845  seqz  12849  1exp  12889  hashnn0pnf  13130  hashprg  13182  hashprgOLD  13183  cats1un  13475  fsumss  14456  sumsnf  14473  fsumsplitsn  14474  sumsn  14475  fsum2dlem  14501  fsumcom2  14505  fsumcom2OLD  14506  ackbijnn  14560  fprodss  14678  fprod2dlem  14710  fprodcom2  14714  fprodcom2OLD  14715  fprodsplitsn  14720  sumeven  15110  sumodd  15111  divalgmod  15129  lcmfunsnlem2lem1  15351  lcmfunsnlem2lem2  15352  phi1  15478  dfphi2  15479  nnnn0modprm0  15511  ramubcl  15722  0ram  15724  ramz  15729  imasvscafn  16197  xpsc0  16220  xpsc1  16221  xpsfrnel2  16225  mreexmrid  16303  2initoinv  16660  2termoinv  16667  gsumress  17276  gsumval2  17280  0nsg  17639  symgextf1lem  17840  symgextf1  17841  pmtrprfval  17907  psgnsn  17940  lsmdisj2  18095  subgdisj1  18104  lt6abl  18296  gsumsnfd  18351  gsumzunsnd  18355  gsumunsnfd  18356  gsum2dlem2  18370  dprdfeq0  18421  dprdsn  18435  dprd2da  18441  pgpfac1lem3a  18475  pgpfaclem2  18481  lsssn0  18948  lspsneq0  19012  lspdisjb  19126  0ring01eq  19271  mplcoe5  19468  coe1tm  19643  frgpcyg  19922  obselocv  20072  obs2ss  20073  mat0dim0  20273  mat0dimid  20274  mat0dimscm  20275  mat1dimscm  20281  mavmul0g  20359  mdet0pr  20398  mdetunilem9  20426  cramer0  20496  pmatcollpw3fi1lem1  20591  basdif0  20757  ordtbas  20996  ordtrest2  21008  cmpfi  21211  refun0  21318  txdis1cn  21438  ptrescn  21442  txkgen  21455  xkoptsub  21457  ordthmeolem  21604  pt1hmeo  21609  filconn  21687  filufint  21724  flimclslem  21788  ptcmplem3  21858  idnghm  22547  iccpnfcnv  22743  iccpnfhmeo  22744  bndth  22757  ivthicc  23227  ovoliunlem1  23270  i1fima2sn  23447  i1f1  23457  itg1addlem4  23466  itg1addlem5  23467  i1fmulc  23470  limcres  23650  limccnp  23655  limccnp2  23656  degltlem1  23832  ply1rem  23923  fta1blem  23928  ig1pdvds  23936  plyeq0lem  23966  plypf1  23968  plyaddlem1  23969  plymullem1  23970  coemulhi  24010  plycj  24033  taylfval  24113  abelthlem3  24187  rlimcnp  24692  wilthlem2  24795  logexprlim  24950  tgldim0eq  25398  edglnl  26038  nbgr1vtx  26254  vtxdginducedm1lem4  26438  clwlkclwwlklem2a4  26898  eucrct2eupth  27105  frgrncvvdeqlem9  27171  nsnlplig  27333  nsnlpligALT  27334  fsumiunle  29575  xrge0tsmsbi  29786  ordtrest2NEW  29969  xrge0iifcnv  29979  xrge0iifhom  29983  esumsnf  30126  esumpr  30128  esumiun  30156  inelpisys  30217  measvunilem0  30276  measvuni  30277  carsggect  30380  omsmeas  30385  plymulx0  30624  repr0  30689  bnj142OLD  30794  bnj98  30937  bnj1442  31117  bnj1452  31120  subfacp1lem5  31166  erdszelem4  31176  erdszelem8  31180  sconnpi1  31221  cvmlift2lem6  31290  cvmlift2lem12  31296  onint1  32448  bj-1nel0  32941  bj-sngltag  32971  bj-projval  32984  tan2h  33401  lindsenlbs  33404  matunitlindf  33407  ptrest  33408  poimirlem23  33432  poimirlem24  33433  poimirlem25  33434  poimirlem28  33437  poimirlem29  33438  poimirlem30  33439  poimirlem31  33440  poimirlem32  33441  prdsbnd  33592  rrnequiv  33634  grpokerinj  33692  rngoueqz  33739  gidsn  33751  0rngo  33826  isdmn3  33873  dibelval2nd  36441  hdmaprnlem9N  37149  hdmap14lem4a  37163  hbtlem5  37698  flcidc  37744  frege133d  38057  radcnvrat  38513  unisnALT  39162  sumsnd  39185  fnchoice  39188  rnsnf  39370  founiiun0  39377  elmapsnd  39396  fsneqrn  39403  infxrpnf  39674  supminfxr2  39699  cncfiooicc  40107  fperdvper  40133  dvmptfprodlem  40159  dvnprodlem1  40161  dvnprodlem2  40162  itgcoscmulx  40185  stoweidlem44  40261  fourierdlem49  40372  fourierdlem56  40379  fourierdlem80  40403  fourierdlem93  40416  fourierdlem101  40424  sge00  40593  sge0sn  40596  sge0snmpt  40600  sge0iunmptlemfi  40630  sge0p1  40631  sge0fodjrnlem  40633  sge0snmptf  40654  sge0splitsn  40658  nnfoctbdjlem  40672  meadjiunlem  40682  ismeannd  40684  caratheodorylem1  40740  isomenndlem  40744  hoidmv1le  40808  hoidmvlelem2  40810  hoidmvlelem3  40811  ovnhoilem1  40815  hoiqssbl  40839  ovnovollem1  40870  ovnovollem2  40871  eldmressn  41203  iccpartltu  41361  sbgoldbo  41675  nnsum3primesprm  41678  bgoldbtbndlem3  41695  c0snmgmhm  41914  zrinitorngc  42000  ldepspr  42262  lmod1zr  42282