Theorem snidg 4605

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

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

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 4569

This theorem is referenced by:  snidb  4606  elsn2g  4609  elinsn  4655  snnzg  4719  sneqrg  4783  selsALT  5388  intidg  5404  eldmressnsn  5983  elsnxp  6249  fvressn  7109  fnsnbg  7112  fvsnun1  7130  fsnunfv  7135  resf1extb  7878  1stconst  8043  2ndconst  8044  curry1  8047  curry2  8050  suppsnop  8121  mapsnd  8827  en1uniel  8969  dif1enlem  9087  unifpw  9258  sucprcreg  9512  djurf1o  9828  cfsuc  10170  elfzomin  13683  hashrabsn1  14327  swrds1  14620  fsumsplitsnun  15708  lcmfunsnlem1  16597  ramub1lem1  16988  basprssdmsets  17182  acsfiindd  18510  mgm1  18617  mnd1id  18739  odf1o1  19538  gsumconst  19900  lspsolv  21133  mat1ghm  22458  mat1mhm  22459  mavmul0  22527  m1detdiag  22572  mdetrlin  22577  mdetrsca  22578  chpmat1dlem  22810  maxlp  23122  cnpdis  23268  conncompid  23406  dislly  23472  locfindis  23505  dfac14lem  23592  txtube  23615  pt1hmeo  23781  ufileu  23894  filufint  23895  uffix  23896  uffixsn  23900  i1fima2sn  25657  ply1rem  26141  noextenddif  27646  noextendlt  27647  noextendgt  27648  cutlt  27938  addsval  27968  negsunif  28061  mulsval  28115  mulsproplem5  28126  mulsproplem6  28127  mulsproplem7  28128  mulsproplem8  28129  mulsuniflem  28155  edglnl  29226  vtxd0nedgb  29572  1loopgrvd2  29587  wlkp1  29763  1wlkdlem2  30223  1conngr  30279  frgrwopregasn  30401  frgrwopregbsn  30402  wlkl0  30452  fconst7v  32708  elrspunsn  33504  mplmulmvr  33698  esplyind  33734  rtelextdg2  33887  esumel  34207  actfunsnrndisj  34765  reprsuc  34775  breprexplema  34790  derangsn  35368  erdszelem4  35392  cvmlift2lem9  35509  fv1stcnv  35975  fv2ndcnv  35976  neibastop2lem  36558  ttcsnssg  36714  ttcsnidg  36715  bj-nsnid  37393  bj-snmoore  37441  ismrer1  38173  elpaddatriN  40263  frlmsnic  42999  kelac2  43511  rngunsnply  43615  brtrclfv2  44172  k0004lem3  44594  projf1o  45644  fsneq  45653  fsneqrn  45658  unirnmapsn  45661  ssmapsn  45663  fconst7  45711  mccllem  46045  limcresiooub  46088  limcresioolb  46089  cnfdmsn  46328  cxpcncf2  46345  dvmptfprodlem  46390  dvnprodlem1  46392  dvnprodlem2  46393  dvnprodlem3  46394  fourierdlem49  46601  prsal  46764  salexct  46780  salgencntex  46789  sge0sn  46825  sge0snmpt  46829  sge0snmptf  46883  caratheodorylem1  46972  hoiprodp1  47034  hoidmv1le  47040  hoidmvlelem1  47041  hoidmvlelem2  47042  hoidmvlelem3  47043  hoidmvlelem4  47044  hspmbllem2  47073  ovnovollem1  47102  ovnovollem2  47103  funressnfv  47503  cfsetsnfsetf  47518  cfsetsnfsetfo  47520  el1fzopredsuc  47786  snlindsntor  48959  lmod1lem1  48975  lmod1lem2  48976  lmod1lem3  48977  lmod1lem4  48978  lmod1lem5  48979  lmod1zr  48981  funcsn  50028