Theorem elsni 4414

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

Syntax hints:   → wi 4   = wceq 1658   ∈ wcel 2166  {csn 4397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-v 3416  df-sn 4398

This theorem is referenced by:  elsn2g  4431  nelsn  4433  elpwunsn  4444  eqoreldif  4445  disjsn2  4466  rabsnifsb  4475  sssn  4575  disjxsn  4867  opth1  5164  sosn  5423  ressn  5912  elsnxp  5918  elsuci  6029  funcnvsn  6172  funopdmsn  6666  fvconst  6682  fnsnr  6683  fmptap  6688  mpt2snif  7014  1stconst  7529  2ndconst  7530  reldmtpos  7625  tpostpos  7637  disjen  8386  map2xp  8399  ac6sfi  8473  ixpfi2  8533  elfi2  8589  fisn  8602  unxpwdom2  8762  cantnfp1lem3  8854  djulf1o  9051  djurf1o  9052  djur  9058  eldju2ndl  9063  eldju2ndr  9064  isfin4-3  9452  dcomex  9584  iundom2g  9677  fpwwe2lem13  9779  canthp1lem2  9790  0tsk  9892  elreal2  10269  ax1rid  10298  ltxrlt  10427  un0addcl  11653  un0mulcl  11654  fzodisjsn  12801  elfzonlteqm1  12839  elfzo0l  12853  elfzr  12876  elfzlmr  12877  seqf1o  13136  seqid3  13139  seqz  13143  1exp  13183  hashnn0pnf  13422  hashprg  13472  cats1un  13811  fsumss  14833  sumsnf  14850  fsumsplitsn  14851  fsum2dlem  14876  fsumcom2  14880  ackbijnn  14934  fprodss  15051  fprod2dlem  15083  fprodcom2  15087  fprodsplitsn  15092  sumeven  15484  sumodd  15485  divalgmod  15503  lcmfunsnlem2lem1  15724  lcmfunsnlem2lem2  15725  phi1  15849  dfphi2  15850  nnnn0modprm0  15882  ramubcl  16093  0ram  16095  ramz  16100  imasvscafn  16550  xpsc0  16573  xpsc1  16574  xpsfrnel2  16578  mreexmrid  16656  2initoinv  17012  2termoinv  17019  gsumress  17629  gsumval2  17633  0nsg  17990  symgextf1lem  18190  symgextf1  18191  pmtrprfval  18257  psgnsn  18291  lsmdisj2  18446  subgdisj1  18455  lt6abl  18649  gsumsnfd  18704  gsumzunsnd  18708  gsumunsnfd  18709  gsum2dlem2  18723  dprdfeq0  18775  dprdsn  18789  dprd2da  18795  pgpfac1lem3a  18829  pgpfaclem2  18835  lsssn0  19304  lspsneq0  19371  lspdisjb  19485  0ring01eq  19632  mplcoe5  19829  coe1tm  20003  frgpcyg  20281  obselocv  20435  obs2ss  20436  mat0dim0  20641  mat0dimid  20642  mat0dimscm  20643  mat1dimscm  20649  mavmul0g  20727  mdet0pr  20766  mdetunilem9  20794  cramer0  20866  pmatcollpw3fi1lem1  20961  basdif0  21128  ordtbas  21367  ordtrest2  21379  cmpfi  21582  refun0  21689  txdis1cn  21809  ptrescn  21813  txkgen  21826  xkoptsub  21828  ordthmeolem  21975  pt1hmeo  21980  filconn  22057  filufint  22094  flimclslem  22158  ptcmplem3  22228  idnghm  22917  iccpnfcnv  23113  iccpnfhmeo  23114  bndth  23127  ivthicc  23624  ovoliunlem1  23668  i1fima2sn  23846  i1f1  23856  itg1addlem4  23865  itg1addlem5  23866  i1fmulc  23869  limcres  24049  limccnp  24054  limccnp2  24055  degltlem1  24231  ply1rem  24322  fta1blem  24327  ig1pdvds  24335  plyeq0lem  24365  plypf1  24367  plyaddlem1  24368  plymullem1  24369  coemulhi  24409  plycj  24432  taylfval  24512  abelthlem3  24586  rlimcnp  25105  wilthlem2  25208  logexprlim  25363  tgldim0eq  25815  edglnl  26442  nbgr1vtx  26655  vtxdginducedm1lem4  26840  clwlkclwwlklem2a4  27326  eucrct2eupthOLD  27623  eucrct2eupth  27624  frgrncvvdeqlem9  27688  nsnlplig  27891  nsnlpligALT  27892  fsumiunle  30122  xrge0tsmsbi  30331  ordtrest2NEW  30514  xrge0iifcnv  30524  xrge0iifhom  30528  esumsnf  30671  esumpr  30673  esumiun  30701  inelpisys  30762  measvunilem0  30821  measvuni  30822  carsggect  30925  omsmeas  30930  plymulx0  31171  repr0  31238  bnj98  31483  bnj1442  31663  bnj1452  31666  subfacp1lem5  31712  erdszelem4  31722  erdszelem8  31726  sconnpi1  31767  cvmlift2lem6  31836  cvmlift2lem12  31842  onint1  32981  bj-1nel0  33463  bj-sngltag  33493  bj-projval  33506  bj-fununsn1  33680  tan2h  33944  lindsenlbs  33948  matunitlindf  33951  ptrest  33952  poimirlem23  33976  poimirlem24  33977  poimirlem25  33978  poimirlem28  33981  poimirlem29  33982  poimirlem30  33983  poimirlem31  33984  poimirlem32  33985  prdsbnd  34134  rrnequiv  34176  grpokerinj  34234  rngoueqz  34281  gidsn  34293  0rngo  34368  isdmn3  34415  dibelval2nd  37227  hdmaprnlem9N  37932  hdmap14lem4a  37946  hbtlem5  38541  flcidc  38587  frege133d  38898  radcnvrat  39353  unisnALT  39980  sumsnd  40003  fnchoice  40006  rnsnf  40178  founiiun0  40185  elmapsnd  40202  fsneqrn  40209  infxrpnf  40469  supminfxr2  40493  cncfiooicc  40902  fperdvper  40928  dvmptfprodlem  40954  dvnprodlem1  40956  dvnprodlem2  40957  itgcoscmulx  40979  stoweidlem44  41055  fourierdlem49  41166  fourierdlem56  41173  fourierdlem80  41197  fourierdlem93  41210  fourierdlem101  41218  sge00  41384  sge0sn  41387  sge0snmpt  41391  sge0iunmptlemfi  41421  sge0p1  41422  sge0fodjrnlem  41424  sge0snmptf  41445  sge0splitsn  41449  nnfoctbdjlem  41463  meadjiunlem  41473  ismeannd  41475  caratheodorylem1  41534  isomenndlem  41538  hoidmv1le  41602  hoidmvlelem2  41604  hoidmvlelem3  41605  ovnhoilem1  41609  hoiqssbl  41633  ovnovollem1  41664  ovnovollem2  41665  eldmressn  41968  iccpartltu  42249  sbgoldbo  42505  nnsum3primesprm  42508  bgoldbtbndlem3  42525  c0snmgmhm  42761  zrinitorngc  42847  ldepspr  43109  lmod1zr  43129