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

Theorem snidg 4351
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 2760 . 2 𝐴 = 𝐴
2 elsng 4335 . 2 (𝐴𝑉 → (𝐴 ∈ {𝐴} ↔ 𝐴 = 𝐴))
31, 2mpbiri 248 1 (𝐴𝑉𝐴 ∈ {𝐴})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632  wcel 2139  {csn 4321
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-sn 4322
This theorem is referenced by:  snidb  4352  elsn2g  4355  elinsn  4389  snnzg  4451  sneqrg  4515  eldmressnsn  5597  elsnxp  5838  elsnxpOLD  5839  fvressn  6592  fsnunfv  6617  1stconst  7433  2ndconst  7434  curry1  7437  curry2  7440  suppsnop  7477  en1uniel  8193  unifpw  8434  sucprcreg  8671  djurf1o  8947  cfsuc  9271  elfzomin  12734  hashrabsn1  13355  swrds1  13651  fsumsplitsnun  14683  lcmfunsnlem1  15552  ramub1lem1  15932  basprssdmsets  16127  acsfiindd  17378  mgm1  17458  mnd1id  17533  odf1o1  18187  gsumconst  18534  lspsolv  19345  mat1ghm  20491  mat1mhm  20492  mavmul0  20560  m1detdiag  20605  mdetrlin  20610  mdetrsca  20611  chpmat1dlem  20842  maxlp  21153  cnpdis  21299  conncompid  21436  dislly  21502  locfindis  21535  dfac14lem  21622  txtube  21645  pt1hmeo  21811  ufileu  21924  filufint  21925  uffix  21926  uffixsn  21930  i1fima2sn  23646  ply1rem  24122  edglnl  26237  vtxd0nedgb  26594  1loopgrvd2  26609  wlkp1  26788  1wlkdlem2  27290  1conngr  27346  frgrwopregasn  27470  frgrwopregbsn  27471  wlkl0  27528  esumel  30418  actfunsnrndisj  30992  reprsuc  31002  breprexplema  31017  derangsn  31459  erdszelem4  31483  cvmlift2lem9  31600  fv1stcnv  31985  fv2ndcnv  31986  noextenddif  32127  noextendlt  32128  noextendgt  32129  neibastop2lem  32661  bj-sels  33256  bj-snmoore  33374  ismrer1  33950  elpaddatriN  35592  kelac2  38137  rngunsnply  38245  brtrclfv2  38521  k0004lem3  38949  projf1o  39885  mapsnd  39887  fsneq  39897  fsneqrn  39902  unirnmapsn  39905  ssmapsn  39907  fconst7  39983  mccllem  40332  limcresiooub  40377  limcresioolb  40378  cnfdmsn  40598  cxpcncf2  40616  dvmptfprodlem  40662  dvnprodlem1  40664  dvnprodlem2  40665  dvnprodlem3  40666  fourierdlem49  40875  prsal  41041  salexct  41055  salgencntex  41064  sge0sn  41099  sge0snmpt  41103  sge0snmptf  41157  caratheodorylem1  41246  hoiprodp1  41308  hoidmv1le  41314  hoidmvlelem1  41315  hoidmvlelem2  41316  hoidmvlelem3  41317  hoidmvlelem4  41318  hspmbllem2  41347  ovnovollem1  41376  ovnovollem2  41377  funressnfv  41714  el1fzopredsuc  41845  snlindsntor  42770  lmod1lem1  42786  lmod1lem2  42787  lmod1lem3  42788  lmod1lem4  42789  lmod1lem5  42790  lmod1zr  42792
  Copyright terms: Public domain W3C validator