Theorem snidg 4631

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  {csn 4594

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-sn 4595

This theorem is used by:  snidb  4632  elsn2g  4635  elinsn  4681  snnzg  4745  sneqrg  4809  selsALT  5427  intidg  5443  eldmressnsn  6028  elsnxp  6299  fsneq  7037  fvressn  7166  fnsnbg  7169  fvsnun1  7187  fsnunfv  7192  resf1extb  7940  1stconst  8104  2ndconst  8105  curry1  8108  curry2  8111  suppsnop  8183  mapsnd  8893  en1uniel  9036  dif1enlem  9154  unifpw  9322  sucprcregOLD  9579  djurf1o  9918  cfsuc  10259  elfzomin  13785  hashrabsn1  14430  swrds1  14728  fsumsplitsnun  15832  lcmfunsnlem1  16720  ramub1lem1  17111  basprssdmsets  17306  acsfiindd  18634  mgm1  18741  mnd1id  18869  odf1o1  19673  gsumconst  20035  lspsolv  21304  mat1ghm  22677  mat1mhm  22678  mavmul0  22746  m1detdiag  22791  mdetrlin  22796  mdetrsca  22797  chpmat1dlem  23029  maxlp  23341  cnpdis  23487  conncompid  23625  dislly  23691  locfindis  23724  dfac14lem  23811  txtube  23834  pt1hmeo  24000  ufileu  24113  filufint  24114  uffix  24115  uffixsn  24119  i1fima2sn  25876  ply1rem  26360  noextenddif  27869  noextendlt  27870  noextendgt  27871  cutlt  28162  addsval  28192  negsunif  28285  mulsval  28339  mulsproplem5  28350  mulsproplem6  28351  mulsproplem7  28352  mulsproplem8  28353  mulsuniflem  28379  lnincplng  29103  edglnl  29530  vtxd0nedgb  29875  1loopgrvd2  29890  wlkp1  30066  1wlkdlem2  30526  1conngr  30582  frgrwopregasn  30704  frgrwopregbsn  30705  wlkl0  30755  fconst7v  33002  elrspunsn  33768  selvply1rhmlemb  33940  mplmulmvr  33960  esplyind  33996  rtelextdg2  34148  esumel  34468  actfunsnrndisj  35024  reprsuc  35034  breprexplema  35049  derangsn  35683  erdszelem4  35707  cvmlift2lem9  35824  fv1stcnv  36290  fv2ndcnv  36291  neibastop2lem  36912  ttcsnssg  37068  ttcsnidg  37069  bj-nsnid  37747  bj-snmoore  37796  ismrer1  38530  elpaddatriN  40618  frlmsnic  43349  kelac2  43833  rngunsnply  43937  brtrclfv2  44494  k0004lem3  44916  projf1o  45955  fsneqrn  45968  unirnmapsn  45971  ssmapsn  45973  fconst7  46020  mccllem  46354  limcresiooub  46397  limcresioolb  46398  cnfdmsn  46637  cxpcncf2  46654  dvmptfprodlem  46699  dvnprodlem1  46701  dvnprodlem2  46702  dvnprodlem3  46703  fourierdlem49  46910  prsal  47073  salexct  47089  salgencntex  47098  sge0sn  47134  sge0snmpt  47138  sge0snmptf  47192  caratheodorylem1  47281  hoiprodp1  47343  hoidmv1le  47349  hoidmvlelem1  47350  hoidmvlelem2  47351  hoidmvlelem3  47352  hoidmvlelem4  47353  hspmbllem2  47382  ovnovollem1  47411  ovnovollem2  47412  funressnfv  47821  cfsetsnfsetf  47836  cfsetsnfsetfo  47838  el1fzopredsuc  48104  snlindsntor  49292  lmod1lem1  49308  lmod1lem2  49309  lmod1lem3  49310  lmod1lem4  49311  lmod1lem5  49312  lmod1zr  49314  funcsn  50360