Theorem snidg 4663

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  {csn 4629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-sn 4630

This theorem is referenced by:  snidb  4664  elsn2g  4667  elinsn  4715  snnzg  4779  sneqrg  4841  selsALT  5440  intidg  5458  eldmressnsn  6025  elsnxp  6291  fvressn  7160  fvsnun1  7180  fsnunfv  7185  1stconst  8086  2ndconst  8087  curry1  8090  curry2  8093  suppsnop  8163  mapsnd  8880  en1uniel  9028  en1unielOLD  9029  dif1enlem  9156  dif1enlemOLD  9157  unifpw  9355  sucprcreg  9596  djurf1o  9908  cfsuc  10252  elfzomin  13704  hashrabsn1  14334  swrds1  14616  fsumsplitsnun  15701  lcmfunsnlem1  16574  ramub1lem1  16959  basprssdmsets  17157  acsfiindd  18506  mgm1  18577  mnd1id  18668  odf1o1  19440  gsumconst  19802  lspsolv  20756  mat1ghm  21985  mat1mhm  21986  mavmul0  22054  m1detdiag  22099  mdetrlin  22104  mdetrsca  22105  chpmat1dlem  22337  maxlp  22651  cnpdis  22797  conncompid  22935  dislly  23001  locfindis  23034  dfac14lem  23121  txtube  23144  pt1hmeo  23310  ufileu  23423  filufint  23424  uffix  23425  uffixsn  23429  i1fima2sn  25197  ply1rem  25681  noextenddif  27171  noextendlt  27172  noextendgt  27173  cutlt  27419  addsval  27446  negsunif  27529  mulsval  27565  mulsproplem5  27576  mulsproplem6  27577  mulsproplem7  27578  mulsproplem8  27579  mulsuniflem  27604  edglnl  28403  vtxd0nedgb  28745  1loopgrvd2  28760  wlkp1  28938  1wlkdlem2  29391  1conngr  29447  frgrwopregasn  29569  frgrwopregbsn  29570  wlkl0  29620  elrspunsn  32547  esumel  33045  actfunsnrndisj  33617  reprsuc  33627  breprexplema  33642  derangsn  34161  erdszelem4  34185  cvmlift2lem9  34302  fv1stcnv  34748  fv2ndcnv  34749  neibastop2lem  35245  bj-nsnid  35951  bj-snmoore  35994  ismrer1  36706  elpaddatriN  38674  fnsnbt  41051  frlmsnic  41110  kelac2  41807  rngunsnply  41915  brtrclfv2  42478  k0004lem3  42900  projf1o  43896  fsneq  43905  fsneqrn  43910  unirnmapsn  43913  ssmapsn  43915  fconst7  43969  mccllem  44313  limcresiooub  44358  limcresioolb  44359  cnfdmsn  44598  cxpcncf2  44615  dvmptfprodlem  44660  dvnprodlem1  44662  dvnprodlem2  44663  dvnprodlem3  44664  fourierdlem49  44871  prsal  45034  salexct  45050  salgencntex  45059  sge0sn  45095  sge0snmpt  45099  sge0snmptf  45153  caratheodorylem1  45242  hoiprodp1  45304  hoidmv1le  45310  hoidmvlelem1  45311  hoidmvlelem2  45312  hoidmvlelem3  45313  hoidmvlelem4  45314  hspmbllem2  45343  ovnovollem1  45372  ovnovollem2  45373  funressnfv  45753  cfsetsnfsetf  45768  cfsetsnfsetfo  45770  el1fzopredsuc  46033  snlindsntor  47152  lmod1lem1  47168  lmod1lem2  47169  lmod1lem3  47170  lmod1lem4  47171  lmod1lem5  47172  lmod1zr  47174