Theorem snidg 4662

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  {csn 4628

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-sn 4629

This theorem is referenced by:  snidb  4663  elsn2g  4666  elinsn  4714  snnzg  4778  sneqrg  4840  selsALT  5439  intidg  5457  eldmressnsn  6024  elsnxp  6290  fvressn  7159  fvsnun1  7179  fsnunfv  7184  1stconst  8085  2ndconst  8086  curry1  8089  curry2  8092  suppsnop  8162  mapsnd  8879  en1uniel  9027  en1unielOLD  9028  dif1enlem  9155  dif1enlemOLD  9156  unifpw  9354  sucprcreg  9595  djurf1o  9907  cfsuc  10251  elfzomin  13703  hashrabsn1  14333  swrds1  14615  fsumsplitsnun  15700  lcmfunsnlem1  16573  ramub1lem1  16958  basprssdmsets  17156  acsfiindd  18505  mgm1  18576  mnd1id  18667  odf1o1  19439  gsumconst  19801  lspsolv  20755  mat1ghm  21984  mat1mhm  21985  mavmul0  22053  m1detdiag  22098  mdetrlin  22103  mdetrsca  22104  chpmat1dlem  22336  maxlp  22650  cnpdis  22796  conncompid  22934  dislly  23000  locfindis  23033  dfac14lem  23120  txtube  23143  pt1hmeo  23309  ufileu  23422  filufint  23423  uffix  23424  uffixsn  23428  i1fima2sn  25196  ply1rem  25680  noextenddif  27168  noextendlt  27169  noextendgt  27170  cutlt  27416  addsval  27443  negsunif  27526  mulsval  27562  mulsproplem5  27573  mulsproplem6  27574  mulsproplem7  27575  mulsproplem8  27576  mulsuniflem  27601  edglnl  28400  vtxd0nedgb  28742  1loopgrvd2  28757  wlkp1  28935  1wlkdlem2  29388  1conngr  29444  frgrwopregasn  29566  frgrwopregbsn  29567  wlkl0  29617  elrspunsn  32542  esumel  33040  actfunsnrndisj  33612  reprsuc  33622  breprexplema  33637  derangsn  34156  erdszelem4  34180  cvmlift2lem9  34297  fv1stcnv  34743  fv2ndcnv  34744  neibastop2lem  35240  bj-nsnid  35946  bj-snmoore  35989  ismrer1  36701  elpaddatriN  38669  fnsnbt  41053  frlmsnic  41112  kelac2  41797  rngunsnply  41905  brtrclfv2  42468  k0004lem3  42890  projf1o  43886  fsneq  43895  fsneqrn  43900  unirnmapsn  43903  ssmapsn  43905  fconst7  43959  mccllem  44303  limcresiooub  44348  limcresioolb  44349  cnfdmsn  44588  cxpcncf2  44605  dvmptfprodlem  44650  dvnprodlem1  44652  dvnprodlem2  44653  dvnprodlem3  44654  fourierdlem49  44861  prsal  45024  salexct  45040  salgencntex  45049  sge0sn  45085  sge0snmpt  45089  sge0snmptf  45143  caratheodorylem1  45232  hoiprodp1  45294  hoidmv1le  45300  hoidmvlelem1  45301  hoidmvlelem2  45302  hoidmvlelem3  45303  hoidmvlelem4  45304  hspmbllem2  45333  ovnovollem1  45362  ovnovollem2  45363  funressnfv  45743  cfsetsnfsetf  45758  cfsetsnfsetfo  45760  el1fzopredsuc  46023  snlindsntor  47142  lmod1lem1  47158  lmod1lem2  47159  lmod1lem3  47160  lmod1lem4  47161  lmod1lem5  47162  lmod1zr  47164