MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elsni Structured version   Visualization version   GIF version

Theorem elsni 4556
Description: There is at most one element in a singleton. (Contributed by NM, 5-Jun-1994.)
Assertion
Ref Expression
elsni (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)

Proof of Theorem elsni
StepHypRef Expression
1 elsng 4553 . 2 (𝐴 ∈ {𝐵} → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
21ibi 270 1 (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2114  {csn 4539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2794
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-sn 4540
This theorem is referenced by:  elsn2g  4577  nelsn  4579  elpwunsn  4595  eqoreldif  4596  disjsn2  4622  rabsnifsb  4632  sssn  4732  disjxsn  5035  opth1  5344  sosn  5615  ressn  6114  elsnxp  6120  elsuci  6235  funcnvsn  6383  funopdmsn  6894  fvconst  6908  fnsnr  6909  fmptap  6914  mposnif  7252  1stconst  7782  2ndconst  7783  reldmtpos  7887  tpostpos  7899  disjen  8662  map2xp  8675  ac6sfi  8750  ixpfi2  8810  elfi2  8866  fisn  8879  unxpwdom2  9040  cantnfp1lem3  9131  djulf1o  9329  djurf1o  9330  djur  9336  eldju2ndl  9341  eldju2ndr  9342  isfin4p1  9726  dcomex  9858  iundom2g  9951  fpwwe2lem13  10053  canthp1lem2  10064  0tsk  10166  elreal2  10543  ax1rid  10572  ltxrlt  10700  un0addcl  11918  un0mulcl  11919  fzodisjsn  13070  elfzonlteqm1  13108  elfzo0l  13122  elfzr  13145  elfzlmr  13146  seqf1o  13407  seqid3  13410  seqz  13414  1exp  13454  hashnn0pnf  13698  hash1elsn  13728  hashprg  13752  cats1un  14074  fsumss  15073  sumsnf  15090  fsumsplitsn  15091  fsum2dlem  15116  fsumcom2  15120  ackbijnn  15174  fprodss  15293  fprod2dlem  15325  fprodcom2  15329  fprodsplitsn  15334  sumeven  15727  sumodd  15728  divalgmod  15746  lcmfunsnlem2lem1  15971  lcmfunsnlem2lem2  15972  phi1  16099  dfphi2  16100  nnnn0modprm0  16132  ramubcl  16343  0ram  16345  ramz  16350  imasvscafn  16801  mreexmrid  16905  2initoinv  17261  2termoinv  17268  gsumress  17883  gsumval2  17887  smndex1basss  18061  smndex1mndlem  18065  0nsg  18312  symgextf1lem  18539  symgextf1  18540  pmtrprfval  18606  psgnsn  18639  lsmdisj2  18799  subgdisj1  18808  lt6abl  19006  gsumsnfd  19062  gsumzunsnd  19067  gsumunsnfd  19068  gsum2dlem2  19082  dprdfeq0  19135  dprdsn  19149  dprd2da  19155  pgpfac1lem3a  19189  pgpfaclem2  19195  ablsimpnosubgd  19217  lsssn0  19710  lspsneq0  19775  lspdisjb  19889  0ring01eq  20035  frgpcyg  20263  obselocv  20415  obs2ss  20416  mplcoe5  20706  coe1tm  20900  mat0dim0  21070  mat0dimid  21071  mat0dimscm  21072  mat1dimscm  21078  mavmul0g  21156  mdet0pr  21195  mdetunilem9  21223  cramer0  21293  pmatcollpw3fi1lem1  21389  basdif0  21556  ordtbas  21795  ordtrest2  21807  cmpfi  22011  refun0  22118  txdis1cn  22238  ptrescn  22242  txkgen  22255  xkoptsub  22257  ordthmeolem  22404  pt1hmeo  22409  filconn  22486  filufint  22523  flimclslem  22587  ptcmplem3  22657  idnghm  23347  iccpnfcnv  23547  iccpnfhmeo  23548  bndth  23561  ivthicc  24060  ovoliunlem1  24104  i1fima2sn  24282  i1f1  24292  itg1addlem4  24301  itg1addlem5  24302  i1fmulc  24305  limcres  24487  limccnp  24492  limccnp2  24493  degltlem1  24671  ply1rem  24762  fta1blem  24767  ig1pdvds  24775  plyeq0lem  24805  plypf1  24807  plyaddlem1  24808  plymullem1  24809  coemulhi  24849  plycj  24872  taylfval  24952  abelthlem3  25026  rlimcnp  25549  wilthlem2  25652  logexprlim  25807  2sqreultblem  26030  tgldim0eq  26295  edglnl  26934  nbgr1vtx  27146  vtxdginducedm1lem4  27330  clwlkclwwlklem2a4  27780  eucrct2eupth  28028  frgrncvvdeqlem9  28090  nsnlplig  28262  nsnlpligALT  28263  fsumiunle  30555  cshw1s2  30644  xrge0tsmsbi  30724  cyc3evpm  30823  pidlnz  30972  lbslsat  31071  lindsunlem  31077  ordtrest2NEW  31240  xrge0iifcnv  31250  xrge0iifhom  31254  esumsnf  31397  esumpr  31399  esumiun  31427  inelpisys  31487  measvunilem0  31546  measvuni  31547  carsggect  31650  omsmeas  31655  plymulx0  31891  repr0  31956  bnj98  32213  bnj1442  32395  bnj1452  32398  subfacp1lem5  32505  erdszelem4  32515  erdszelem8  32519  sconnpi1  32560  cvmlift2lem6  32629  cvmlift2lem12  32635  fmla0xp  32704  onint1  33871  bj-1nel0  34351  bj-sngltag  34380  bj-projval  34393  bj-elsn0  34531  bj-fununsn1  34629  bj-isrvec  34669  tan2h  35007  lindsenlbs  35010  matunitlindf  35013  ptrest  35014  poimirlem23  35038  poimirlem24  35039  poimirlem25  35040  poimirlem28  35043  poimirlem29  35044  poimirlem30  35045  poimirlem31  35046  poimirlem32  35047  prdsbnd  35189  rrnequiv  35231  grpokerinj  35289  rngoueqz  35336  gidsn  35348  0rngo  35423  isdmn3  35470  dibelval2nd  38406  hdmaprnlem9N  39111  hdmap14lem4a  39125  0prjspnrel  39543  hbtlem5  40002  flcidc  40048  frege133d  40396  radcnvrat  40952  unisnALT  41566  sumsnd  41589  fnchoice  41592  rnsnf  41748  founiiun0  41755  elmapsnd  41771  fsneqrn  41778  infxrpnf  42023  supminfxr2  42047  cncfiooicc  42475  fperdvper  42500  dvmptfprodlem  42525  dvnprodlem1  42527  dvnprodlem2  42528  itgcoscmulx  42550  stoweidlem44  42625  fourierdlem49  42736  fourierdlem56  42743  fourierdlem80  42767  fourierdlem93  42780  fourierdlem101  42788  sge00  42954  sge0sn  42957  sge0snmpt  42961  sge0iunmptlemfi  42991  sge0p1  42992  sge0fodjrnlem  42994  sge0snmptf  43015  sge0splitsn  43019  nnfoctbdjlem  43033  meadjiunlem  43043  ismeannd  43045  caratheodorylem1  43104  isomenndlem  43108  hoidmv1le  43172  hoidmvlelem2  43174  hoidmvlelem3  43175  ovnhoilem1  43179  hoiqssbl  43203  ovnovollem1  43234  ovnovollem2  43235  eldmressn  43568  iccpartltu  43881  sbgoldbo  44244  nnsum3primesprm  44247  bgoldbtbndlem3  44264  c0snmgmhm  44477  zrinitorngc  44563  ldepspr  44821  lmod1zr  44841
  Copyright terms: Public domain W3C validator