Theorem snidg 4627

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  {csn 4592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-sn 4593

This theorem is referenced by:  snidb  4628  elsn2g  4631  elinsn  4677  snnzg  4741  sneqrg  4806  selsALT  5402  intidg  5420  eldmressnsn  5998  elsnxp  6267  fvressn  7137  fnsnbg  7141  fvsnun1  7159  fsnunfv  7164  resf1extb  7913  1stconst  8082  2ndconst  8083  curry1  8086  curry2  8089  suppsnop  8160  mapsnd  8862  en1uniel  9003  dif1enlem  9126  dif1enlemOLD  9127  unifpw  9313  sucprcreg  9561  djurf1o  9873  cfsuc  10217  elfzomin  13705  hashrabsn1  14346  swrds1  14638  fsumsplitsnun  15728  lcmfunsnlem1  16614  ramub1lem1  17004  basprssdmsets  17198  acsfiindd  18519  mgm1  18592  mnd1id  18714  odf1o1  19509  gsumconst  19871  lspsolv  21060  mat1ghm  22377  mat1mhm  22378  mavmul0  22446  m1detdiag  22491  mdetrlin  22496  mdetrsca  22497  chpmat1dlem  22729  maxlp  23041  cnpdis  23187  conncompid  23325  dislly  23391  locfindis  23424  dfac14lem  23511  txtube  23534  pt1hmeo  23700  ufileu  23813  filufint  23814  uffix  23815  uffixsn  23819  i1fima2sn  25588  ply1rem  26078  noextenddif  27587  noextendlt  27588  noextendgt  27589  cutlt  27847  addsval  27876  negsunif  27968  mulsval  28019  mulsproplem5  28030  mulsproplem6  28031  mulsproplem7  28032  mulsproplem8  28033  mulsuniflem  28059  edglnl  29077  vtxd0nedgb  29423  1loopgrvd2  29438  wlkp1  29616  1wlkdlem2  30074  1conngr  30130  frgrwopregasn  30252  frgrwopregbsn  30253  wlkl0  30303  elrspunsn  33407  rtelextdg2  33724  esumel  34044  actfunsnrndisj  34603  reprsuc  34613  breprexplema  34628  derangsn  35164  erdszelem4  35188  cvmlift2lem9  35305  fv1stcnv  35771  fv2ndcnv  35772  neibastop2lem  36355  bj-nsnid  37065  bj-snmoore  37108  ismrer1  37839  elpaddatriN  39804  frlmsnic  42535  kelac2  43061  rngunsnply  43165  brtrclfv2  43723  k0004lem3  44145  projf1o  45198  fsneq  45207  fsneqrn  45212  unirnmapsn  45215  ssmapsn  45217  fconst7  45265  mccllem  45602  limcresiooub  45647  limcresioolb  45648  cnfdmsn  45887  cxpcncf2  45904  dvmptfprodlem  45949  dvnprodlem1  45951  dvnprodlem2  45952  dvnprodlem3  45953  fourierdlem49  46160  prsal  46323  salexct  46339  salgencntex  46348  sge0sn  46384  sge0snmpt  46388  sge0snmptf  46442  caratheodorylem1  46531  hoiprodp1  46593  hoidmv1le  46599  hoidmvlelem1  46600  hoidmvlelem2  46601  hoidmvlelem3  46602  hoidmvlelem4  46603  hspmbllem2  46632  ovnovollem1  46661  ovnovollem2  46662  funressnfv  47048  cfsetsnfsetf  47063  cfsetsnfsetfo  47065  el1fzopredsuc  47330  snlindsntor  48464  lmod1lem1  48480  lmod1lem2  48481  lmod1lem3  48482  lmod1lem4  48483  lmod1lem5  48484  lmod1zr  48486  funcsn  49534