Theorem elsni 4587

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2113  {csn 4570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-sn 4571

This theorem is referenced by:  elsn2g  4606  nelsn  4608  elpwunsn  4624  eqoreldif  4625  disjsn2  4651  rabsnifsb  4661  sssn  4762  disjxsn  5062  opth1  5370  sosn  5641  ressn  6139  elsnxp  6145  elsuci  6260  funcnvsn  6407  funopdmsn  6915  fvconst  6929  fnsnr  6930  fmptap  6935  mposnif  7271  1stconst  7798  2ndconst  7799  reldmtpos  7903  tpostpos  7915  disjen  8677  map2xp  8690  ac6sfi  8765  ixpfi2  8825  elfi2  8881  fisn  8894  unxpwdom2  9055  cantnfp1lem3  9146  djulf1o  9344  djurf1o  9345  djur  9351  eldju2ndl  9356  eldju2ndr  9357  isfin4p1  9740  dcomex  9872  iundom2g  9965  fpwwe2lem13  10067  canthp1lem2  10078  0tsk  10180  elreal2  10557  ax1rid  10586  ltxrlt  10714  un0addcl  11933  un0mulcl  11934  fzodisjsn  13078  elfzonlteqm1  13116  elfzo0l  13130  elfzr  13153  elfzlmr  13154  seqf1o  13414  seqid3  13417  seqz  13421  1exp  13461  hashnn0pnf  13705  hash1elsn  13735  hashprg  13759  cats1un  14086  fsumss  15085  sumsnf  15102  fsumsplitsn  15103  fsum2dlem  15128  fsumcom2  15132  ackbijnn  15186  fprodss  15305  fprod2dlem  15337  fprodcom2  15341  fprodsplitsn  15346  sumeven  15741  sumodd  15742  divalgmod  15760  lcmfunsnlem2lem1  15985  lcmfunsnlem2lem2  15986  phi1  16113  dfphi2  16114  nnnn0modprm0  16146  ramubcl  16357  0ram  16359  ramz  16364  imasvscafn  16813  mreexmrid  16917  2initoinv  17273  2termoinv  17280  gsumress  17895  gsumval2  17899  smndex1basss  18073  smndex1mndlem  18077  0nsg  18324  symgextf1lem  18551  symgextf1  18552  pmtrprfval  18618  psgnsn  18651  lsmdisj2  18811  subgdisj1  18820  lt6abl  19018  gsumsnfd  19074  gsumzunsnd  19079  gsumunsnfd  19080  gsum2dlem2  19094  dprdfeq0  19147  dprdsn  19161  dprd2da  19167  pgpfac1lem3a  19201  pgpfaclem2  19207  ablsimpnosubgd  19229  lsssn0  19722  lspsneq0  19787  lspdisjb  19901  0ring01eq  20047  mplcoe5  20252  coe1tm  20444  frgpcyg  20723  obselocv  20875  obs2ss  20876  mat0dim0  21079  mat0dimid  21080  mat0dimscm  21081  mat1dimscm  21087  mavmul0g  21165  mdet0pr  21204  mdetunilem9  21232  cramer0  21302  pmatcollpw3fi1lem1  21397  basdif0  21564  ordtbas  21803  ordtrest2  21815  cmpfi  22019  refun0  22126  txdis1cn  22246  ptrescn  22250  txkgen  22263  xkoptsub  22265  ordthmeolem  22412  pt1hmeo  22417  filconn  22494  filufint  22531  flimclslem  22595  ptcmplem3  22665  idnghm  23355  iccpnfcnv  23551  iccpnfhmeo  23552  bndth  23565  ivthicc  24062  ovoliunlem1  24106  i1fima2sn  24284  i1f1  24294  itg1addlem4  24303  itg1addlem5  24304  i1fmulc  24307  limcres  24487  limccnp  24492  limccnp2  24493  degltlem1  24669  ply1rem  24760  fta1blem  24765  ig1pdvds  24773  plyeq0lem  24803  plypf1  24805  plyaddlem1  24806  plymullem1  24807  coemulhi  24847  plycj  24870  taylfval  24950  abelthlem3  25024  rlimcnp  25546  wilthlem2  25649  logexprlim  25804  2sqreultblem  26027  tgldim0eq  26292  edglnl  26931  nbgr1vtx  27143  vtxdginducedm1lem4  27327  clwlkclwwlklem2a4  27778  eucrct2eupth  28027  frgrncvvdeqlem9  28089  nsnlplig  28261  nsnlpligALT  28262  fsumiunle  30549  cshw1s2  30638  xrge0tsmsbi  30697  cyc3evpm  30796  lbslsat  31018  lindsunlem  31024  ordtrest2NEW  31170  xrge0iifcnv  31180  xrge0iifhom  31184  esumsnf  31327  esumpr  31329  esumiun  31357  inelpisys  31417  measvunilem0  31476  measvuni  31477  carsggect  31580  omsmeas  31585  plymulx0  31821  repr0  31886  bnj98  32143  bnj1442  32325  bnj1452  32328  subfacp1lem5  32435  erdszelem4  32445  erdszelem8  32449  sconnpi1  32490  cvmlift2lem6  32559  cvmlift2lem12  32565  fmla0xp  32634  onint1  33801  bj-1nel0  34270  bj-sngltag  34299  bj-projval  34312  bj-elsn0  34451  bj-fununsn1  34539  bj-isrvec  34579  tan2h  34888  lindsenlbs  34891  matunitlindf  34894  ptrest  34895  poimirlem23  34919  poimirlem24  34920  poimirlem25  34921  poimirlem28  34924  poimirlem29  34925  poimirlem30  34926  poimirlem31  34927  poimirlem32  34928  prdsbnd  35075  rrnequiv  35117  grpokerinj  35175  rngoueqz  35222  gidsn  35234  0rngo  35309  isdmn3  35356  dibelval2nd  38292  hdmaprnlem9N  38997  hdmap14lem4a  39011  0prjspnrel  39275  hbtlem5  39734  flcidc  39780  frege133d  40116  radcnvrat  40652  unisnALT  41266  sumsnd  41289  fnchoice  41292  rnsnf  41450  founiiun0  41457  elmapsnd  41473  fsneqrn  41480  infxrpnf  41727  supminfxr2  41751  cncfiooicc  42183  fperdvper  42209  dvmptfprodlem  42235  dvnprodlem1  42237  dvnprodlem2  42238  itgcoscmulx  42260  stoweidlem44  42336  fourierdlem49  42447  fourierdlem56  42454  fourierdlem80  42478  fourierdlem93  42491  fourierdlem101  42499  sge00  42665  sge0sn  42668  sge0snmpt  42672  sge0iunmptlemfi  42702  sge0p1  42703  sge0fodjrnlem  42705  sge0snmptf  42726  sge0splitsn  42730  nnfoctbdjlem  42744  meadjiunlem  42754  ismeannd  42756  caratheodorylem1  42815  isomenndlem  42819  hoidmv1le  42883  hoidmvlelem2  42885  hoidmvlelem3  42886  ovnhoilem1  42890  hoiqssbl  42914  ovnovollem1  42945  ovnovollem2  42946  eldmressn  43279  iccpartltu  43592  sbgoldbo  43959  nnsum3primesprm  43962  bgoldbtbndlem3  43979  c0snmgmhm  44192  zrinitorngc  44278  ldepspr  44535  lmod1zr  44555