Theorem snidg 4599

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  {csn 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-sn 4568

This theorem is referenced by:  snidb  4600  elsn2g  4603  elinsn  4646  snnzg  4710  sneqrg  4770  sels  5334  eldmressnsn  5895  elsnxp  6142  fvressn  6924  fvsnun1  6944  fsnunfv  6949  1stconst  7795  2ndconst  7796  curry1  7799  curry2  7802  suppsnop  7844  mapsnd  8450  en1uniel  8581  unifpw  8827  sucprcreg  9065  djurf1o  9342  cfsuc  9679  elfzomin  13110  hashrabsn1  13736  swrds1  14028  fsumsplitsnun  15110  lcmfunsnlem1  15981  ramub1lem1  16362  basprssdmsets  16549  acsfiindd  17787  mgm1  17868  mnd1id  17953  odf1o1  18697  gsumconst  19054  lspsolv  19915  mat1ghm  21092  mat1mhm  21093  mavmul0  21161  m1detdiag  21206  mdetrlin  21211  mdetrsca  21212  chpmat1dlem  21443  maxlp  21755  cnpdis  21901  conncompid  22039  dislly  22105  locfindis  22138  dfac14lem  22225  txtube  22248  pt1hmeo  22414  ufileu  22527  filufint  22528  uffix  22529  uffixsn  22533  i1fima2sn  24281  ply1rem  24757  edglnl  26928  vtxd0nedgb  27270  1loopgrvd2  27285  wlkp1  27463  1wlkdlem2  27917  1conngr  27973  frgrwopregasn  28095  frgrwopregbsn  28096  wlkl0  28146  esumel  31306  actfunsnrndisj  31876  reprsuc  31886  breprexplema  31901  derangsn  32417  erdszelem4  32441  cvmlift2lem9  32558  fv1stcnv  33020  fv2ndcnv  33021  noextenddif  33175  noextendlt  33176  noextendgt  33177  neibastop2lem  33708  bj-nsnid  34365  bj-snmoore  34408  ismrer1  35131  elpaddatriN  36954  fnsnbt  39169  frlmsnic  39198  kelac2  39714  rngunsnply  39822  brtrclfv2  40121  k0004lem3  40548  projf1o  41508  fsneq  41518  fsneqrn  41523  unirnmapsn  41526  ssmapsn  41528  fconst7  41588  mccllem  41927  limcresiooub  41972  limcresioolb  41973  cnfdmsn  42214  cxpcncf2  42232  dvmptfprodlem  42278  dvnprodlem1  42280  dvnprodlem2  42281  dvnprodlem3  42282  fourierdlem49  42489  prsal  42652  salexct  42666  salgencntex  42675  sge0sn  42710  sge0snmpt  42714  sge0snmptf  42768  caratheodorylem1  42857  hoiprodp1  42919  hoidmv1le  42925  hoidmvlelem1  42926  hoidmvlelem2  42927  hoidmvlelem3  42928  hoidmvlelem4  42929  hspmbllem2  42958  ovnovollem1  42987  ovnovollem2  42988  funressnfv  43327  el1fzopredsuc  43574  snlindsntor  44575  lmod1lem1  44591  lmod1lem2  44592  lmod1lem3  44593  lmod1lem4  44594  lmod1lem5  44595  lmod1zr  44597