Theorem elsni 4333

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

Syntax hints:   → wi 4   = wceq 1631   ∈ wcel 2145  {csn 4316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-sn 4317

This theorem is referenced by:  elsn2g  4349  nelsn  4351  elpwunsn  4362  eqoreldif  4363  disjsn2  4384  rabsnifsb  4393  sssn  4492  disjxsn  4780  opth1  5071  sosn  5326  ressn  5813  elsnxp  5819  elsuci  5932  funcnvsn  6077  funopdmsn  6556  fvconst  6572  fnsnr  6573  fmptap  6578  mpt2snif  6899  1stconst  7414  2ndconst  7415  reldmtpos  7510  tpostpos  7522  disjen  8271  map2xp  8284  ac6sfi  8358  ixpfi2  8418  elfi2  8474  fisn  8487  unxpwdom2  8647  cantnfp1lem3  8739  djulf1o  8936  djurf1o  8937  djur  8943  eldju2ndl  8948  eldju2ndr  8949  isfin4-3  9337  dcomex  9469  iundom2g  9562  fpwwe2lem13  9664  canthp1lem2  9675  0tsk  9777  elreal2  10153  ax1rid  10182  ltxrlt  10308  un0addcl  11526  un0mulcl  11527  fzodisjsn  12707  elfzonlteqm1  12745  elfzo0l  12759  elfzr  12782  elfzlmr  12783  seqf1o  13042  seqid3  13045  seqz  13049  1exp  13089  hashnn0pnf  13327  hashprg  13377  hashprgOLD  13378  cats1un  13677  fsumss  14657  sumsnf  14674  fsumsplitsn  14675  sumsn  14676  fsum2dlem  14702  fsumcom2  14706  ackbijnn  14760  fprodss  14878  fprod2dlem  14910  fprodcom2  14914  fprodsplitsn  14919  sumeven  15311  sumodd  15312  divalgmod  15330  lcmfunsnlem2lem1  15552  lcmfunsnlem2lem2  15553  phi1  15678  dfphi2  15679  nnnn0modprm0  15711  ramubcl  15922  0ram  15924  ramz  15929  imasvscafn  16398  xpsc0  16421  xpsc1  16422  xpsfrnel2  16426  mreexmrid  16504  2initoinv  16860  2termoinv  16867  gsumress  17477  gsumval2  17481  0nsg  17840  symgextf1lem  18040  symgextf1  18041  pmtrprfval  18107  psgnsn  18140  lsmdisj2  18295  subgdisj1  18304  lt6abl  18496  gsumsnfd  18551  gsumzunsnd  18555  gsumunsnfd  18556  gsum2dlem2  18570  dprdfeq0  18622  dprdsn  18636  dprd2da  18642  pgpfac1lem3a  18676  pgpfaclem2  18682  lsssn0  19151  lspsneq0  19218  lspdisjb  19332  0ring01eq  19479  mplcoe5  19676  coe1tm  19851  frgpcyg  20130  obselocv  20282  obs2ss  20283  mat0dim0  20484  mat0dimid  20485  mat0dimscm  20486  mat1dimscm  20492  mavmul0g  20570  mdet0pr  20609  mdetunilem9  20637  cramer0  20709  pmatcollpw3fi1lem1  20804  basdif0  20971  ordtbas  21210  ordtrest2  21222  cmpfi  21425  refun0  21532  txdis1cn  21652  ptrescn  21656  txkgen  21669  xkoptsub  21671  ordthmeolem  21818  pt1hmeo  21823  filconn  21900  filufint  21937  flimclslem  22001  ptcmplem3  22071  idnghm  22760  iccpnfcnv  22956  iccpnfhmeo  22957  bndth  22970  ivthicc  23439  ovoliunlem1  23483  i1fima2sn  23660  i1f1  23670  itg1addlem4  23679  itg1addlem5  23680  i1fmulc  23683  limcres  23863  limccnp  23868  limccnp2  23869  degltlem1  24045  ply1rem  24136  fta1blem  24141  ig1pdvds  24149  plyeq0lem  24179  plypf1  24181  plyaddlem1  24182  plymullem1  24183  coemulhi  24223  plycj  24246  taylfval  24326  abelthlem3  24400  rlimcnp  24906  wilthlem2  25009  logexprlim  25164  tgldim0eq  25612  edglnl  26253  nbgr1vtx  26470  vtxdginducedm1lem4  26666  clwlkclwwlklem2a4  27140  eucrct2eupth  27418  frgrncvvdeqlem9  27482  nsnlplig  27668  nsnlpligALT  27669  fsumiunle  29908  xrge0tsmsbi  30119  ordtrest2NEW  30302  xrge0iifcnv  30312  xrge0iifhom  30316  esumsnf  30459  esumpr  30461  esumiun  30489  inelpisys  30550  measvunilem0  30609  measvuni  30610  carsggect  30713  omsmeas  30718  plymulx0  30957  repr0  31022  bnj98  31268  bnj1442  31448  bnj1452  31451  subfacp1lem5  31497  erdszelem4  31507  erdszelem8  31511  sconnpi1  31552  cvmlift2lem6  31621  cvmlift2lem12  31627  onint1  32778  bj-1nel0  33265  bj-sngltag  33295  bj-projval  33308  tan2h  33727  lindsenlbs  33730  matunitlindf  33733  ptrest  33734  poimirlem23  33758  poimirlem24  33759  poimirlem25  33760  poimirlem28  33763  poimirlem29  33764  poimirlem30  33765  poimirlem31  33766  poimirlem32  33767  prdsbnd  33917  rrnequiv  33959  grpokerinj  34017  rngoueqz  34064  gidsn  34076  0rngo  34151  isdmn3  34198  dibelval2nd  36955  hdmaprnlem9N  37660  hdmap14lem4a  37674  hbtlem5  38217  flcidc  38263  frege133d  38576  radcnvrat  39032  unisnALT  39677  sumsnd  39700  fnchoice  39703  rnsnf  39883  founiiun0  39890  elmapsnd  39907  fsneqrn  39914  infxrpnf  40183  supminfxr2  40208  cncfiooicc  40618  fperdvper  40644  dvmptfprodlem  40670  dvnprodlem1  40672  dvnprodlem2  40673  itgcoscmulx  40695  stoweidlem44  40771  fourierdlem49  40882  fourierdlem56  40889  fourierdlem80  40913  fourierdlem93  40926  fourierdlem101  40934  sge00  41103  sge0sn  41106  sge0snmpt  41110  sge0iunmptlemfi  41140  sge0p1  41141  sge0fodjrnlem  41143  sge0snmptf  41164  sge0splitsn  41168  nnfoctbdjlem  41182  meadjiunlem  41192  ismeannd  41194  caratheodorylem1  41253  isomenndlem  41257  hoidmv1le  41321  hoidmvlelem2  41323  hoidmvlelem3  41324  ovnhoilem1  41328  hoiqssbl  41352  ovnovollem1  41383  ovnovollem2  41384  eldmressn  41716  iccpartltu  41882  sbgoldbo  42196  nnsum3primesprm  42199  bgoldbtbndlem3  42216  c0snmgmhm  42435  zrinitorngc  42521  ldepspr  42783  lmod1zr  42803