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

Theorem snidg 4152
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 2609 . 2 𝐴 = 𝐴
2 elsng 4138 . 2 (𝐴𝑉 → (𝐴 ∈ {𝐴} ↔ 𝐴 = 𝐴))
31, 2mpbiri 246 1 (𝐴𝑉𝐴 ∈ {𝐴})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wcel 1976  {csn 4124
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-sn 4125
This theorem is referenced by:  snidb  4153  elsn2g  4156  snnzg  4250  sneqrg  4305  eldmressnsn  5346  elsnxp  5580  elsnxpOLD  5581  fvressn  6312  fsnunfv  6336  1stconst  7129  2ndconst  7130  curry1  7133  curry2  7136  suppsnop  7173  en1uniel  7891  unifpw  8129  sucprcreg  8366  cfsuc  8939  elfzomin  12361  hashrabsn1  12976  swrds1  13249  lcmfunsnlem1  15134  ramub1lem1  15514  acsfiindd  16946  mgm1  17026  mnd1id  17101  odf1o1  17756  gsumconst  18103  lspsolv  18910  mat1ghm  20050  mat1mhm  20051  mavmul0  20119  m1detdiag  20164  mdetrlin  20169  mdetrsca  20170  chpmat1dlem  20401  maxlp  20703  cnpdis  20849  concompid  20986  dislly  21052  locfindis  21085  dfac14lem  21172  txtube  21195  pt1hmeo  21361  ufileu  21475  filufint  21476  uffix  21477  uffixsn  21481  i1fima2sn  23170  ply1rem  23644  1conngra  25969  vdgr1d  26196  vdgr1a  26199  eupap1  26269  esumel  29242  derangsn  30212  erdszelem4  30236  cvmlift2lem9  30353  fv1stcnv  30731  fv2ndcnv  30732  neibastop2lem  31331  bj-sels  31946  ismrer1  32610  elpaddatriN  33910  kelac2  36456  rngunsnply  36565  brtrclfv2  36841  k0004lem3  37270  projf1o  38184  mapsnd  38186  fsneq  38196  fsneqrn  38201  unirnmapsn  38204  ssmapsn  38206  mccllem  38468  limcresiooub  38513  limcresioolb  38514  cnfdmsn  38571  cxpcncf2  38590  dvmptfprodlem  38638  dvnprodlem1  38640  dvnprodlem2  38641  dvnprodlem3  38642  fourierdlem49  38852  prsal  39018  salexct  39032  salgencntex  39041  sge0sn  39076  sge0snmpt  39080  sge0snmptf  39134  caratheodorylem1  39220  hoiprodp1  39282  hoidmv1le  39288  hoidmvlelem1  39289  hoidmvlelem2  39290  hoidmvlelem3  39291  hoidmvlelem4  39292  hspmbllem2  39321  ovnovollem1  39350  ovnovollem2  39351  funressnfv  39661  el1fzopredsuc  39753  vtxd0nedgb  40705  1loopgrvd2  40720  1wlkp1  40892  11wlkdlem2  41307  1conngr  41363  snlindsntor  42056  lmod1lem1  42072  lmod1lem2  42073  lmod1lem3  42074  lmod1lem4  42075  lmod1lem5  42076  lmod1zr  42078
  Copyright terms: Public domain W3C validator