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

Theorem elsni 4227
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 4224 . 2 (𝐴 ∈ {𝐵} → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
21ibi 256 1 (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wcel 2030  {csn 4210
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-sn 4211
This theorem is referenced by:  elsn2g  4243  nelsn  4245  elpwunsn  4256  eqoreldif  4257  eqoreldifOLD  4258  disjsn2  4279  rabsnifsb  4289  sssn  4390  disjxsn  4678  opth1  4973  sosn  5222  ressn  5709  elsnxp  5715  elsuci  5829  funcnvsn  5974  funopdmsn  6455  fvconst  6471  fnsnr  6472  fmptap  6477  mpt2snif  6796  1stconst  7310  2ndconst  7311  reldmtpos  7405  tpostpos  7417  disjen  8158  map2xp  8171  ac6sfi  8245  ixpfi2  8305  elfi2  8361  fisn  8374  unxpwdom2  8534  cantnfp1lem3  8615  isfin4-3  9175  dcomex  9307  iundom2g  9400  fpwwe2lem13  9502  canthp1lem2  9513  0tsk  9615  elreal2  9991  ax1rid  10020  ltxrlt  10146  un0addcl  11364  un0mulcl  11365  fzodisjsn  12545  elfzonlteqm1  12583  elfzo0l  12598  elfzr  12621  elfzlmr  12622  seqf1o  12882  seqid3  12885  seqz  12889  1exp  12929  hashnn0pnf  13170  hashprg  13220  hashprgOLD  13221  cats1un  13521  fsumss  14500  sumsnf  14517  fsumsplitsn  14518  sumsn  14519  fsum2dlem  14545  fsumcom2  14549  fsumcom2OLD  14550  ackbijnn  14604  fprodss  14722  fprod2dlem  14754  fprodcom2  14758  fprodcom2OLD  14759  fprodsplitsn  14764  sumeven  15157  sumodd  15158  divalgmod  15176  lcmfunsnlem2lem1  15398  lcmfunsnlem2lem2  15399  phi1  15525  dfphi2  15526  nnnn0modprm0  15558  ramubcl  15769  0ram  15771  ramz  15776  imasvscafn  16244  xpsc0  16267  xpsc1  16268  xpsfrnel2  16272  mreexmrid  16350  2initoinv  16707  2termoinv  16714  gsumress  17323  gsumval2  17327  0nsg  17686  symgextf1lem  17886  symgextf1  17887  pmtrprfval  17953  psgnsn  17986  lsmdisj2  18141  subgdisj1  18150  lt6abl  18342  gsumsnfd  18397  gsumzunsnd  18401  gsumunsnfd  18402  gsum2dlem2  18416  dprdfeq0  18467  dprdsn  18481  dprd2da  18487  pgpfac1lem3a  18521  pgpfaclem2  18527  lsssn0  18996  lspsneq0  19060  lspdisjb  19174  0ring01eq  19319  mplcoe5  19516  coe1tm  19691  frgpcyg  19970  obselocv  20120  obs2ss  20121  mat0dim0  20321  mat0dimid  20322  mat0dimscm  20323  mat1dimscm  20329  mavmul0g  20407  mdet0pr  20446  mdetunilem9  20474  cramer0  20544  pmatcollpw3fi1lem1  20639  basdif0  20805  ordtbas  21044  ordtrest2  21056  cmpfi  21259  refun0  21366  txdis1cn  21486  ptrescn  21490  txkgen  21503  xkoptsub  21505  ordthmeolem  21652  pt1hmeo  21657  filconn  21734  filufint  21771  flimclslem  21835  ptcmplem3  21905  idnghm  22594  iccpnfcnv  22790  iccpnfhmeo  22791  bndth  22804  ivthicc  23273  ovoliunlem1  23316  i1fima2sn  23492  i1f1  23502  itg1addlem4  23511  itg1addlem5  23512  i1fmulc  23515  limcres  23695  limccnp  23700  limccnp2  23701  degltlem1  23877  ply1rem  23968  fta1blem  23973  ig1pdvds  23981  plyeq0lem  24011  plypf1  24013  plyaddlem1  24014  plymullem1  24015  coemulhi  24055  plycj  24078  taylfval  24158  abelthlem3  24232  rlimcnp  24737  wilthlem2  24840  logexprlim  24995  tgldim0eq  25443  edglnl  26083  nbgr1vtx  26299  vtxdginducedm1lem4  26494  clwlkclwwlklem2a4  26963  eucrct2eupth  27223  frgrncvvdeqlem9  27287  nsnlplig  27463  nsnlpligALT  27464  fsumiunle  29703  xrge0tsmsbi  29914  ordtrest2NEW  30097  xrge0iifcnv  30107  xrge0iifhom  30111  esumsnf  30254  esumpr  30256  esumiun  30284  inelpisys  30345  measvunilem0  30404  measvuni  30405  carsggect  30508  omsmeas  30513  plymulx0  30752  repr0  30817  bnj98  31063  bnj1442  31243  bnj1452  31246  subfacp1lem5  31292  erdszelem4  31302  erdszelem8  31306  sconnpi1  31347  cvmlift2lem6  31416  cvmlift2lem12  31422  onint1  32573  bj-1nel0  33066  bj-sngltag  33096  bj-projval  33109  tan2h  33531  lindsenlbs  33534  matunitlindf  33537  ptrest  33538  poimirlem23  33562  poimirlem24  33563  poimirlem25  33564  poimirlem28  33567  poimirlem29  33568  poimirlem30  33569  poimirlem31  33570  poimirlem32  33571  prdsbnd  33722  rrnequiv  33764  grpokerinj  33822  rngoueqz  33869  gidsn  33881  0rngo  33956  isdmn3  34003  dibelval2nd  36758  hdmaprnlem9N  37466  hdmap14lem4a  37480  hbtlem5  38015  flcidc  38061  frege133d  38374  radcnvrat  38830  unisnALT  39476  sumsnd  39499  fnchoice  39502  rnsnf  39684  founiiun0  39691  elmapsnd  39710  fsneqrn  39717  infxrpnf  39987  supminfxr2  40012  cncfiooicc  40425  fperdvper  40451  dvmptfprodlem  40477  dvnprodlem1  40479  dvnprodlem2  40480  itgcoscmulx  40503  stoweidlem44  40579  fourierdlem49  40690  fourierdlem56  40697  fourierdlem80  40721  fourierdlem93  40734  fourierdlem101  40742  sge00  40911  sge0sn  40914  sge0snmpt  40918  sge0iunmptlemfi  40948  sge0p1  40949  sge0fodjrnlem  40951  sge0snmptf  40972  sge0splitsn  40976  nnfoctbdjlem  40990  meadjiunlem  41000  ismeannd  41002  caratheodorylem1  41061  isomenndlem  41065  hoidmv1le  41129  hoidmvlelem2  41131  hoidmvlelem3  41132  ovnhoilem1  41136  hoiqssbl  41160  ovnovollem1  41191  ovnovollem2  41192  eldmressn  41524  iccpartltu  41686  sbgoldbo  42000  nnsum3primesprm  42003  bgoldbtbndlem3  42020  c0snmgmhm  42239  zrinitorngc  42325  ldepspr  42587  lmod1zr  42607
  Copyright terms: Public domain W3C validator