Theorem pwidg 4581

Description: A set is an element of its power set. (Contributed by Stefan O'Rear, 1-Feb-2015.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)

Assertion

Ref	Expression
pwidg	⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ 𝒫 𝐴)

Proof of Theorem pwidg

Step	Hyp	Ref	Expression
1		elex 3475	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
2		ssidd 3936	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ 𝐴)
3	1, 2	elpwd 4566	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ 𝒫 𝐴)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  Vcvv 3454  𝒫 cpw 4560

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-pw 4562

This theorem is used by:  pwidb  4583  pwid  4584  axpweq  5316  knatar  7390  pwssfi  9220  brwdom2  9594  pwwf  9842  rankpwi  9859  canthp1lem2  10765  canthp1  10766  mremre  17803  submre  17804  baspartn  23302  fctop  23352  cctop  23354  ppttop  23355  epttop  23357  isopn3  23414  mretopd  23440  tsmsfbas  24477  exsslsb  34299  gsumesum  34761  esumcst  34765  pwsiga  34832  prsiga  34833  sigainb  34839  pwldsys  34860  ldgenpisyslem1  34866  carsggect  35020  ex-sategoelel  36353  neibastop1  37325  neibastop2lem  37326  topdifinfindis  38461  elrfi  43898  dssmapnvod  45212  ntrk0kbimka  45231  clsk3nimkb  45232  neik0pk1imk0  45239  ntrclscls00  45258  ntrneicls00  45281  dvnprodlem3  47163  caragenunidm  47723  tmachlem-tpopen  48156