Theorem snidg 4617

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-sn 4585

This theorem is used by:  snidb  4618  elsn2g  4621  elinsn  4667  snnzg  4731  sneqrg  4793  selsALT  5408  intidg  5424  eldmressnsn  6012  elsnxp  6294  fsneq  7034  fvressn  7166  fnsnbg  7169  fvsnun1  7187  fsnunfv  7192  resf1extb  7946  1stconst  8113  2ndconst  8114  curry1  8117  curry2  8120  suppsnop  8198  mapsnd  8917  en1uniel  9060  dif1enlem  9178  unifpw  9347  sucprcregOLD  9604  djurf1o  9997  cfsuc  10338  elfzomin  13875  hashrabsn1  14521  swrds1  14820  fsumsplitsnun  15926  lcmfunsnlem1  16817  ramub1lem1  17209  basprssdmsets  17404  acsfiindd  18732  mgm1  18841  mnd1id  18979  odf1o1  19791  gsumconst  20153  lspsolv  21426  mat1ghm  22803  mat1mhm  22804  mavmul0  22872  m1detdiag  22917  mdetrlin  22922  mdetrsca  22923  chpmat1dlem  23158  maxlp  23470  cnpdis  23616  conncompid  23754  dislly  23821  locfindis  23854  dfac14lem  23941  txtube  23964  pt1hmeo  24130  ufileu  24243  filufint  24244  uffix  24245  uffixsn  24249  i1fima2sn  26006  ply1rem  26489  noextenddif  28030  noextendlt  28031  noextendgt  28032  cutlt  28323  addsval  28353  negsunif  28446  mulsval  28500  mulsproplem5  28511  mulsproplem6  28512  mulsproplem7  28513  mulsproplem8  28514  mulsuniflem  28540  lnincplng  29267  edglnl  29726  vtxd0nedgb  30074  1loopgrvd2  30089  wlkp1  30265  1wlkdlem2  30734  1conngr  30800  frgrwopregasn  30922  frgrwopregbsn  30923  wlkl0  30973  fconst7v  33261  elrspunsn  34025  selvply1rhmlemb  34197  mplmulmvr  34217  esplyind  34253  rtelextdg2  34405  esumel  34725  actfunsnrndisj  35280  reprsuc  35290  breprexplema  35305  derangsn  36021  erdszelem4  36045  cvmlift2lem9  36162  fv1stcnv  36633  fv2ndcnv  36634  neibastop2lem  37240  ttcsnssg  37396  ttcsnidg  37397  bj-nsnid  38077  bj-snmoore  38126  ismrer1  38865  elpaddatriN  40953  frlmsnic  43697  kelac2  44160  rngunsnply  44264  brtrclfv2  44820  k0004lem3  45242  projf1o  46304  fsneqrn  46317  unirnmapsn  46320  ssmapsn  46322  fconst7  46369  mccllem  46702  limcresiooub  46745  limcresioolb  46746  cnfdmsn  46985  cxpcncf2  47002  dvmptfprodlem  47047  dvnprodlem1  47049  dvnprodlem2  47050  dvnprodlem3  47051  fourierdlem49  47258  prsal  47421  salexct  47437  salgencntex  47446  sge0sn  47482  sge0snmpt  47486  sge0snmptf  47540  caratheodorylem1  47629  hoiprodp1  47691  hoidmv1le  47697  hoidmvlelem1  47698  hoidmvlelem2  47699  hoidmvlelem3  47700  hoidmvlelem4  47701  hspmbllem2  47730  ovnovollem1  47759  ovnovollem2  47760  funressnfv  48206  cfsetsnfsetf  48221  cfsetsnfsetfo  48223  el1fzopredsuc  48489  snlindsntor  49676  lmod1lem1  49692  lmod1lem2  49693  lmod1lem3  49694  lmod1lem4  49695  lmod1lem5  49696  lmod1zr  49698  funcsn  50772