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

Theorem elsni 4170
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 4167 . 2 (𝐴 ∈ {𝐵} → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
21ibi 256 1 (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  wcel 1987  {csn 4153
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3191  df-sn 4154
This theorem is referenced by:  elsn2g  4186  nelsn  4188  elpwunsn  4200  eqoreldif  4201  eqoreldifOLD  4202  disjsn2  4222  rabsnifsb  4232  sssn  4331  disjxsn  4611  opth1  4909  sosn  5154  ressn  5635  elsnxp  5641  elsuci  5755  funcnvsn  5899  funopdmsn  6375  fvconst  6391  fnsnb  6392  fmptap  6396  mpt2snif  6714  1stconst  7217  2ndconst  7218  reldmtpos  7312  tpostpos  7324  disjen  8069  map2xp  8082  ac6sfi  8156  ixpfi2  8216  elfi2  8272  fisn  8285  unxpwdom2  8445  cantnfp1lem3  8529  isfin4-3  9089  dcomex  9221  iundom2g  9314  fpwwe2lem13  9416  canthp1lem2  9427  0tsk  9529  elreal2  9905  ax1rid  9934  ltxrlt  10060  un0addcl  11278  un0mulcl  11279  fzodisjsn  12454  elfzonlteqm1  12492  elfzo0l  12507  elfzr  12529  elfzlmr  12530  seqf1o  12790  seqid3  12793  seqz  12797  1exp  12837  hashnn0pnf  13078  hashprg  13130  hashprgOLD  13131  cats1un  13421  fsumss  14397  sumsnf  14414  fsumsplitsn  14415  sumsn  14416  fsum2dlem  14440  fsumcom2  14444  fsumcom2OLD  14445  ackbijnn  14496  fprodss  14614  fprod2dlem  14646  fprodcom2  14650  fprodcom2OLD  14651  fprodsplitsn  14656  sumeven  15045  sumodd  15046  divalgmod  15064  lcmfunsnlem2lem1  15286  lcmfunsnlem2lem2  15287  phi1  15413  dfphi2  15414  nnnn0modprm0  15446  ramubcl  15657  0ram  15659  ramz  15664  imasvscafn  16129  xpsc0  16152  xpsc1  16153  xpsfrnel2  16157  mreexmrid  16235  2initoinv  16592  2termoinv  16599  gsumress  17208  gsumval2  17212  0nsg  17571  symgextf1lem  17772  symgextf1  17773  pmtrprfval  17839  psgnsn  17872  lsmdisj2  18027  subgdisj1  18036  lt6abl  18228  gsumsnfd  18283  gsumzunsnd  18287  gsumunsnfd  18288  gsum2dlem2  18302  dprdfeq0  18353  dprdsn  18367  dprd2da  18373  pgpfac1lem3a  18407  pgpfaclem2  18413  lsssn0  18880  lspsneq0  18944  lspdisjb  19058  0ring01eq  19203  mplcoe5  19400  coe1tm  19575  frgpcyg  19854  obselocv  20004  obs2ss  20005  mat0dim0  20205  mat0dimid  20206  mat0dimscm  20207  mat1dimscm  20213  mavmul0g  20291  mdet0pr  20330  mdetunilem9  20358  cramer0  20428  pmatcollpw3fi1lem1  20523  basdif0  20681  ordtbas  20919  ordtrest2  20931  cmpfi  21134  refun0  21241  txdis1cn  21361  ptrescn  21365  txkgen  21378  xkoptsub  21380  ordthmeolem  21527  pt1hmeo  21532  filconn  21610  filufint  21647  flimclslem  21711  ptcmplem3  21781  idnghm  22470  iccpnfcnv  22666  iccpnfhmeo  22667  bndth  22680  ivthicc  23150  ovoliunlem1  23193  i1fima2sn  23370  i1f1  23380  itg1addlem4  23389  itg1addlem5  23390  i1fmulc  23393  limcres  23573  limccnp  23578  limccnp2  23579  degltlem1  23753  ply1rem  23844  fta1blem  23849  ig1pdvds  23857  plyeq0lem  23887  plypf1  23889  plyaddlem1  23890  plymullem1  23891  coemulhi  23931  plycj  23954  taylfval  24034  abelthlem3  24108  rlimcnp  24609  wilthlem2  24712  logexprlim  24867  tgldim0eq  25315  nbgr1vtx  26158  clwlkclwwlklem2a4  26782  eucrct2eupth  26988  frgrncvvdeqlemC  27053  nsnlplig  27204  xrge0tsmsbi  29595  ordtrest2NEW  29775  xrge0iifcnv  29785  xrge0iifhom  29789  esumsnf  29931  esumpr  29933  esumiun  29961  inelpisys  30022  measvunilem0  30081  measvuni  30082  carsggect  30185  omsmeas  30190  plymulx0  30428  brepr0  30482  bnj142OLD  30537  bnj98  30680  bnj1442  30860  bnj1452  30863  subfacp1lem5  30909  erdszelem4  30919  erdszelem8  30923  sconnpi1  30964  cvmlift2lem6  31033  cvmlift2lem12  31039  onint1  32125  bj-1nel0  32623  bj-sngltag  32653  bj-projval  32666  tan2h  33068  lindsenlbs  33071  matunitlindf  33074  ptrest  33075  poimirlem23  33099  poimirlem24  33100  poimirlem25  33101  poimirlem28  33104  poimirlem29  33105  poimirlem30  33106  poimirlem31  33107  poimirlem32  33108  prdsbnd  33259  rrnequiv  33301  grpokerinj  33359  rngoueqz  33406  gidsn  33418  0rngo  33493  isdmn3  33540  dibelval2nd  35956  hdmaprnlem9N  36664  hdmap14lem4a  36678  hbtlem5  37214  flcidc  37260  frege133d  37573  radcnvrat  38030  unisnALT  38680  sumsnd  38703  fnchoice  38706  rnsnf  38875  founiiun0  38882  elmapsnd  38901  fsneqrn  38908  cncfiooicc  39438  fperdvper  39466  dvmptfprodlem  39492  dvnprodlem1  39494  dvnprodlem2  39495  itgcoscmulx  39518  stoweidlem44  39594  fourierdlem49  39705  fourierdlem56  39712  fourierdlem80  39736  fourierdlem93  39749  fourierdlem101  39757  sge00  39926  sge0sn  39929  sge0snmpt  39933  sge0iunmptlemfi  39963  sge0p1  39964  sge0fodjrnlem  39966  sge0snmptf  39987  sge0splitsn  39991  nnfoctbdjlem  40005  meadjiunlem  40015  ismeannd  40017  caratheodorylem1  40073  isomenndlem  40077  hoidmv1le  40141  hoidmvlelem2  40143  hoidmvlelem3  40144  ovnhoilem1  40148  hoiqssbl  40172  ovnovollem1  40203  ovnovollem2  40204  eldmressn  40533  iccpartltu  40685  nnsum3primesprm  40993  bgoldbtbndlem3  41010  c0snmgmhm  41228  zrinitorngc  41314  ldepspr  41576  lmod1zr  41596
  Copyright terms: Public domain W3C validator