Theorem snidg 4619

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  {csn 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-sn 4583

This theorem is referenced by:  snidb  4620  elsn2g  4623  elinsn  4669  snnzg  4733  sneqrg  4797  selsALT  5396  intidg  5412  eldmressnsn  5991  elsnxp  6257  fvressn  7117  fnsnbg  7120  fvsnun1  7138  fsnunfv  7143  resf1extb  7886  1stconst  8052  2ndconst  8053  curry1  8056  curry2  8059  suppsnop  8130  mapsnd  8836  en1uniel  8978  dif1enlem  9096  unifpw  9267  sucprcreg  9521  djurf1o  9837  cfsuc  10179  elfzomin  13665  hashrabsn1  14309  swrds1  14602  fsumsplitsnun  15690  lcmfunsnlem1  16576  ramub1lem1  16966  basprssdmsets  17160  acsfiindd  18488  mgm1  18595  mnd1id  18717  odf1o1  19513  gsumconst  19875  lspsolv  21110  mat1ghm  22439  mat1mhm  22440  mavmul0  22508  m1detdiag  22553  mdetrlin  22558  mdetrsca  22559  chpmat1dlem  22791  maxlp  23103  cnpdis  23249  conncompid  23387  dislly  23453  locfindis  23486  dfac14lem  23573  txtube  23596  pt1hmeo  23762  ufileu  23875  filufint  23876  uffix  23877  uffixsn  23881  i1fima2sn  25649  ply1rem  26139  noextenddif  27648  noextendlt  27649  noextendgt  27650  cutlt  27940  addsval  27970  negsunif  28063  mulsval  28117  mulsproplem5  28128  mulsproplem6  28129  mulsproplem7  28130  mulsproplem8  28131  mulsuniflem  28157  edglnl  29228  vtxd0nedgb  29574  1loopgrvd2  29589  wlkp1  29765  1wlkdlem2  30225  1conngr  30281  frgrwopregasn  30403  frgrwopregbsn  30404  wlkl0  30454  fconst7v  32709  elrspunsn  33521  mplmulmvr  33715  esplyind  33751  rtelextdg2  33904  esumel  34224  actfunsnrndisj  34782  reprsuc  34792  breprexplema  34807  derangsn  35383  erdszelem4  35407  cvmlift2lem9  35524  fv1stcnv  35990  fv2ndcnv  35991  neibastop2lem  36573  bj-nsnid  37312  bj-snmoore  37360  ismrer1  38083  elpaddatriN  40173  frlmsnic  42904  kelac2  43416  rngunsnply  43520  brtrclfv2  44077  k0004lem3  44499  projf1o  45549  fsneq  45558  fsneqrn  45563  unirnmapsn  45566  ssmapsn  45568  fconst7  45616  mccllem  45951  limcresiooub  45994  limcresioolb  45995  cnfdmsn  46234  cxpcncf2  46251  dvmptfprodlem  46296  dvnprodlem1  46298  dvnprodlem2  46299  dvnprodlem3  46300  fourierdlem49  46507  prsal  46670  salexct  46686  salgencntex  46695  sge0sn  46731  sge0snmpt  46735  sge0snmptf  46789  caratheodorylem1  46878  hoiprodp1  46940  hoidmv1le  46946  hoidmvlelem1  46947  hoidmvlelem2  46948  hoidmvlelem3  46949  hoidmvlelem4  46950  hspmbllem2  46979  ovnovollem1  47008  ovnovollem2  47009  funressnfv  47397  cfsetsnfsetf  47412  cfsetsnfsetfo  47414  el1fzopredsuc  47679  snlindsntor  48825  lmod1lem1  48841  lmod1lem2  48842  lmod1lem3  48843  lmod1lem4  48844  lmod1lem5  48845  lmod1zr  48847  funcsn  49894