Theorem snidg 4206

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

Step	Hyp	Ref	Expression
1		eqid 2622	. 2 ⊢ 𝐴 = 𝐴
2		elsng 4191	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐴} ↔ 𝐴 = 𝐴))
3	1, 2	mpbiri 248	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴})

Syntax hints:   → wi 4   = wceq 1483   ∈ wcel 1990  {csn 4177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-sn 4178

This theorem is referenced by:  snidb  4207  elsn2g  4210  elinsn  4245  snnzg  4308  sneqrg  4370  eldmressnsn  5439  elsnxp  5677  elsnxpOLD  5678  fvressn  6429  fsnunfv  6453  1stconst  7265  2ndconst  7266  curry1  7269  curry2  7272  suppsnop  7309  en1uniel  8028  unifpw  8269  sucprcreg  8506  cfsuc  9079  elfzomin  12539  hashrabsn1  13163  swrds1  13451  fsumsplitsnun  14484  lcmfunsnlem1  15350  ramub1lem1  15730  basprssdmsets  15925  acsfiindd  17177  mgm1  17257  mnd1id  17332  odf1o1  17987  gsumconst  18334  lspsolv  19143  mat1ghm  20289  mat1mhm  20290  mavmul0  20358  m1detdiag  20403  mdetrlin  20408  mdetrsca  20409  chpmat1dlem  20640  maxlp  20951  cnpdis  21097  conncompid  21234  dislly  21300  locfindis  21333  dfac14lem  21420  txtube  21443  pt1hmeo  21609  ufileu  21723  filufint  21724  uffix  21725  uffixsn  21729  i1fima2sn  23447  ply1rem  23923  edglnl  26038  vtxd0nedgb  26384  1loopgrvd2  26399  wlkp1  26578  1wlkdlem2  26998  1conngr  27054  frgrwopregasn  27180  frgrwopregbsn  27181  esumel  30109  actfunsnrndisj  30683  reprsuc  30693  breprexplema  30708  derangsn  31152  erdszelem4  31176  cvmlift2lem9  31293  fv1stcnv  31680  fv2ndcnv  31681  noextenddif  31821  noextendlt  31822  noextendgt  31823  neibastop2lem  32355  bj-sels  32950  bj-snmoore  33068  ismrer1  33637  elpaddatriN  35089  kelac2  37635  rngunsnply  37743  brtrclfv2  38019  k0004lem3  38447  projf1o  39386  mapsnd  39388  fsneq  39398  fsneqrn  39403  unirnmapsn  39406  ssmapsn  39408  fconst7  39484  mccllem  39829  limcresiooub  39874  limcresioolb  39875  cnfdmsn  40095  cxpcncf2  40113  dvmptfprodlem  40159  dvnprodlem1  40161  dvnprodlem2  40162  dvnprodlem3  40163  fourierdlem49  40372  prsal  40538  salexct  40552  salgencntex  40561  sge0sn  40596  sge0snmpt  40600  sge0snmptf  40654  caratheodorylem1  40740  hoiprodp1  40802  hoidmv1le  40808  hoidmvlelem1  40809  hoidmvlelem2  40810  hoidmvlelem3  40811  hoidmvlelem4  40812  hspmbllem2  40841  ovnovollem1  40870  ovnovollem2  40871  funressnfv  41208  el1fzopredsuc  41335  snlindsntor  42260  lmod1lem1  42276  lmod1lem2  42277  lmod1lem3  42278  lmod1lem4  42279  lmod1lem5  42280  lmod1zr  42282