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

Theorem snidg 4589
Description: A set is a member of its singleton. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 28-Oct-2003.)
Assertion
Ref Expression
snidg (𝐴𝑉𝐴 ∈ {𝐴})

Proof of Theorem snidg
StepHypRef Expression
1 eqid 2818 . 2 𝐴 = 𝐴
2 elsng 4571 . 2 (𝐴𝑉 → (𝐴 ∈ {𝐴} ↔ 𝐴 = 𝐴))
31, 2mpbiri 259 1 (𝐴𝑉𝐴 ∈ {𝐴})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wcel 2105  {csn 4557
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 2790
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 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-sn 4558
This theorem is referenced by:  snidb  4590  elsn2g  4593  elinsn  4638  snnzg  4702  sneqrg  4762  sels  5324  eldmressnsn  5888  elsnxp  6135  fvressn  6916  fvsnun1  6936  fsnunfv  6941  1stconst  7784  2ndconst  7785  curry1  7788  curry2  7791  suppsnop  7833  mapsnd  8438  en1uniel  8569  unifpw  8815  sucprcreg  9053  djurf1o  9330  cfsuc  9667  elfzomin  13097  hashrabsn1  13723  swrds1  14016  fsumsplitsnun  15098  lcmfunsnlem1  15969  ramub1lem1  16350  basprssdmsets  16537  acsfiindd  17775  mgm1  17856  mnd1id  17941  odf1o1  18626  gsumconst  18983  lspsolv  19844  mat1ghm  21020  mat1mhm  21021  mavmul0  21089  m1detdiag  21134  mdetrlin  21139  mdetrsca  21140  chpmat1dlem  21371  maxlp  21683  cnpdis  21829  conncompid  21967  dislly  22033  locfindis  22066  dfac14lem  22153  txtube  22176  pt1hmeo  22342  ufileu  22455  filufint  22456  uffix  22457  uffixsn  22461  i1fima2sn  24208  ply1rem  24684  edglnl  26855  vtxd0nedgb  27197  1loopgrvd2  27212  wlkp1  27390  1wlkdlem2  27844  1conngr  27900  frgrwopregasn  28022  frgrwopregbsn  28023  wlkl0  28073  esumel  31205  actfunsnrndisj  31775  reprsuc  31785  breprexplema  31800  derangsn  32314  erdszelem4  32338  cvmlift2lem9  32455  fv1stcnv  32917  fv2ndcnv  32918  noextenddif  33072  noextendlt  33073  noextendgt  33074  neibastop2lem  33605  bj-nsnid  34256  bj-snmoore  34299  ismrer1  34997  elpaddatriN  36819  fnsnbt  38998  frlmsnic  39027  kelac2  39543  rngunsnply  39651  brtrclfv2  39950  k0004lem3  40377  projf1o  41335  fsneq  41345  fsneqrn  41350  unirnmapsn  41353  ssmapsn  41355  fconst7  41415  mccllem  41754  limcresiooub  41799  limcresioolb  41800  cnfdmsn  42041  cxpcncf2  42059  dvmptfprodlem  42105  dvnprodlem1  42107  dvnprodlem2  42108  dvnprodlem3  42109  fourierdlem49  42317  prsal  42480  salexct  42494  salgencntex  42503  sge0sn  42538  sge0snmpt  42542  sge0snmptf  42596  caratheodorylem1  42685  hoiprodp1  42747  hoidmv1le  42753  hoidmvlelem1  42754  hoidmvlelem2  42755  hoidmvlelem3  42756  hoidmvlelem4  42757  hspmbllem2  42786  ovnovollem1  42815  ovnovollem2  42816  funressnfv  43155  el1fzopredsuc  43402  snlindsntor  44454  lmod1lem1  44470  lmod1lem2  44471  lmod1lem3  44472  lmod1lem4  44473  lmod1lem5  44474  lmod1zr  44476
  Copyright terms: Public domain W3C validator