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

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

Proof of Theorem elsni
StepHypRef Expression
1 elsng 4573 . 2 (𝐴 ∈ {𝐵} → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
21ibi 268 1 (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wcel 2105  {csn 4559
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-sn 4560
This theorem is referenced by:  elsn2g  4595  nelsn  4597  elpwunsn  4615  eqoreldif  4616  disjsn2  4642  rabsnifsb  4652  sssn  4753  disjxsn  5051  opth1  5359  sosn  5632  ressn  6130  elsnxp  6136  elsuci  6251  funcnvsn  6398  funopdmsn  6905  fvconst  6919  fnsnr  6920  fmptap  6925  mposnif  7257  1stconst  7786  2ndconst  7787  reldmtpos  7891  tpostpos  7903  disjen  8663  map2xp  8676  ac6sfi  8751  ixpfi2  8811  elfi2  8867  fisn  8880  unxpwdom2  9041  cantnfp1lem3  9132  djulf1o  9330  djurf1o  9331  djur  9337  eldju2ndl  9342  eldju2ndr  9343  isfin4p1  9726  dcomex  9858  iundom2g  9951  fpwwe2lem13  10053  canthp1lem2  10064  0tsk  10166  elreal2  10543  ax1rid  10572  ltxrlt  10700  un0addcl  11919  un0mulcl  11920  fzodisjsn  13065  elfzonlteqm1  13103  elfzo0l  13117  elfzr  13140  elfzlmr  13141  seqf1o  13401  seqid3  13404  seqz  13408  1exp  13448  hashnn0pnf  13692  hash1elsn  13722  hashprg  13746  cats1un  14073  fsumss  15072  sumsnf  15089  fsumsplitsn  15090  fsum2dlem  15115  fsumcom2  15119  ackbijnn  15173  fprodss  15292  fprod2dlem  15324  fprodcom2  15328  fprodsplitsn  15333  sumeven  15728  sumodd  15729  divalgmod  15747  lcmfunsnlem2lem1  15972  lcmfunsnlem2lem2  15973  phi1  16100  dfphi2  16101  nnnn0modprm0  16133  ramubcl  16344  0ram  16346  ramz  16351  imasvscafn  16800  mreexmrid  16904  2initoinv  17260  2termoinv  17267  gsumress  17882  gsumval2  17886  0nsg  18261  symgextf1lem  18479  symgextf1  18480  pmtrprfval  18546  psgnsn  18579  lsmdisj2  18739  subgdisj1  18748  lt6abl  18946  gsumsnfd  19002  gsumzunsnd  19007  gsumunsnfd  19008  gsum2dlem2  19022  dprdfeq0  19075  dprdsn  19089  dprd2da  19095  pgpfac1lem3a  19129  pgpfaclem2  19135  ablsimpnosubgd  19157  lsssn0  19650  lspsneq0  19715  lspdisjb  19829  0ring01eq  19974  mplcoe5  20179  coe1tm  20371  frgpcyg  20650  obselocv  20802  obs2ss  20803  mat0dim0  21006  mat0dimid  21007  mat0dimscm  21008  mat1dimscm  21014  mavmul0g  21092  mdet0pr  21131  mdetunilem9  21159  cramer0  21229  pmatcollpw3fi1lem1  21324  basdif0  21491  ordtbas  21730  ordtrest2  21742  cmpfi  21946  refun0  22053  txdis1cn  22173  ptrescn  22177  txkgen  22190  xkoptsub  22192  ordthmeolem  22339  pt1hmeo  22344  filconn  22421  filufint  22458  flimclslem  22522  ptcmplem3  22592  idnghm  23281  iccpnfcnv  23477  iccpnfhmeo  23478  bndth  23491  ivthicc  23988  ovoliunlem1  24032  i1fima2sn  24210  i1f1  24220  itg1addlem4  24229  itg1addlem5  24230  i1fmulc  24233  limcres  24413  limccnp  24418  limccnp2  24419  degltlem1  24595  ply1rem  24686  fta1blem  24691  ig1pdvds  24699  plyeq0lem  24729  plypf1  24731  plyaddlem1  24732  plymullem1  24733  coemulhi  24773  plycj  24796  taylfval  24876  abelthlem3  24950  rlimcnp  25471  wilthlem2  25574  logexprlim  25729  2sqreultblem  25952  tgldim0eq  26217  edglnl  26856  nbgr1vtx  27068  vtxdginducedm1lem4  27252  clwlkclwwlklem2a4  27703  eucrct2eupth  27952  frgrncvvdeqlem9  28014  nsnlplig  28186  nsnlpligALT  28187  fsumiunle  30473  cshw1s2  30562  xrge0tsmsbi  30621  cyc3evpm  30720  lbslsat  30914  lindsunlem  30920  ordtrest2NEW  31066  xrge0iifcnv  31076  xrge0iifhom  31080  esumsnf  31223  esumpr  31225  esumiun  31253  inelpisys  31313  measvunilem0  31372  measvuni  31373  carsggect  31476  omsmeas  31481  plymulx0  31717  repr0  31782  bnj98  32039  bnj1442  32219  bnj1452  32222  subfacp1lem5  32329  erdszelem4  32339  erdszelem8  32343  sconnpi1  32384  cvmlift2lem6  32453  cvmlift2lem12  32459  fmla0xp  32528  onint1  33695  bj-1nel0  34164  bj-sngltag  34193  bj-projval  34206  bj-elsn0  34340  bj-fununsn1  34428  bj-isrvec  34464  tan2h  34766  lindsenlbs  34769  matunitlindf  34772  ptrest  34773  poimirlem23  34797  poimirlem24  34798  poimirlem25  34799  poimirlem28  34802  poimirlem29  34803  poimirlem30  34804  poimirlem31  34805  poimirlem32  34806  prdsbnd  34954  rrnequiv  34996  grpokerinj  35054  rngoueqz  35101  gidsn  35113  0rngo  35188  isdmn3  35235  dibelval2nd  38170  hdmaprnlem9N  38875  hdmap14lem4a  38889  0prjspnrel  39149  hbtlem5  39608  flcidc  39654  frege133d  39990  radcnvrat  40526  unisnALT  41140  sumsnd  41163  fnchoice  41166  rnsnf  41324  founiiun0  41331  elmapsnd  41347  fsneqrn  41354  infxrpnf  41601  supminfxr2  41625  cncfiooicc  42057  fperdvper  42083  dvmptfprodlem  42109  dvnprodlem1  42111  dvnprodlem2  42112  itgcoscmulx  42134  stoweidlem44  42210  fourierdlem49  42321  fourierdlem56  42328  fourierdlem80  42352  fourierdlem93  42365  fourierdlem101  42373  sge00  42539  sge0sn  42542  sge0snmpt  42546  sge0iunmptlemfi  42576  sge0p1  42577  sge0fodjrnlem  42579  sge0snmptf  42600  sge0splitsn  42604  nnfoctbdjlem  42618  meadjiunlem  42628  ismeannd  42630  caratheodorylem1  42689  isomenndlem  42693  hoidmv1le  42757  hoidmvlelem2  42759  hoidmvlelem3  42760  ovnhoilem1  42764  hoiqssbl  42788  ovnovollem1  42819  ovnovollem2  42820  eldmressn  43153  iccpartltu  43432  sbgoldbo  43799  nnsum3primesprm  43802  bgoldbtbndlem3  43819  smndex1basss  43975  smndex1mndlem  43979  c0snmgmhm  44083  zrinitorngc  44169  ldepspr  44426  lmod1zr  44446
  Copyright terms: Public domain W3C validator