Theorem snidg 4153

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 2610	. 2 ⊢ 𝐴 = 𝐴
2		elsng 4139	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐴} ↔ 𝐴 = 𝐴))
3	1, 2	mpbiri 247	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴})

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977  {csn 4125

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-sn 4126

This theorem is referenced by:  snidb  4154  elsn2g  4157  snnzg  4251  sneqrg  4310  eldmressnsn  5359  elsnxp  5594  elsnxpOLD  5595  fvressn  6334  fsnunfv  6358  1stconst  7152  2ndconst  7153  curry1  7156  curry2  7159  suppsnop  7196  en1uniel  7914  unifpw  8152  sucprcreg  8389  cfsuc  8962  elfzomin  12406  hashrabsn1  13024  swrds1  13303  lcmfunsnlem1  15188  ramub1lem1  15568  acsfiindd  17000  mgm1  17080  mnd1id  17155  odf1o1  17810  gsumconst  18157  lspsolv  18964  mat1ghm  20108  mat1mhm  20109  mavmul0  20177  m1detdiag  20222  mdetrlin  20227  mdetrsca  20228  chpmat1dlem  20459  maxlp  20761  cnpdis  20907  concompid  21044  dislly  21110  locfindis  21143  dfac14lem  21230  txtube  21253  pt1hmeo  21419  ufileu  21533  filufint  21534  uffix  21535  uffixsn  21539  i1fima2sn  23253  ply1rem  23727  1conngra  26203  vdgr1d  26430  vdgr1a  26433  eupap1  26503  esumel  29436  derangsn  30406  erdszelem4  30430  cvmlift2lem9  30547  fv1stcnv  30925  fv2ndcnv  30926  neibastop2lem  31525  bj-sels  32143  ismrer1  32807  elpaddatriN  34107  kelac2  36653  rngunsnply  36762  brtrclfv2  37038  k0004lem3  37467  projf1o  38381  mapsnd  38383  fsneq  38393  fsneqrn  38398  unirnmapsn  38401  ssmapsn  38403  mccllem  38664  limcresiooub  38709  limcresioolb  38710  cnfdmsn  38767  cxpcncf2  38786  dvmptfprodlem  38834  dvnprodlem1  38836  dvnprodlem2  38837  dvnprodlem3  38838  fourierdlem49  39048  prsal  39214  salexct  39228  salgencntex  39237  sge0sn  39272  sge0snmpt  39276  sge0snmptf  39330  caratheodorylem1  39416  hoiprodp1  39478  hoidmv1le  39484  hoidmvlelem1  39485  hoidmvlelem2  39486  hoidmvlelem3  39487  hoidmvlelem4  39488  hspmbllem2  39517  ovnovollem1  39546  ovnovollem2  39547  funressnfv  39857  el1fzopredsuc  39948  vtxd0nedgb  40703  1loopgrvd2  40718  1wlkp1  40890  11wlkdlem2  41305  1conngr  41361  snlindsntor  42054  lmod1lem1  42070  lmod1lem2  42071  lmod1lem3  42072  lmod1lem4  42073  lmod1lem5  42074  lmod1zr  42076