Theorem pwidg 4583

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 3476	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
2		ssidd 3961	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ 𝐴)
3	1, 2	elpwd 4569	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ 𝒫 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2143  Vcvv 3455  𝒫 cpw 4563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-ss 3923  df-pw 4565

This theorem is referenced by:  pwidb  4585  pwid  4586  axpweq  5323  knatar  7357  pwssfi  9162  brwdom2  9536  pwwf  9780  rankpwi  9796  canthp1lem2  10639  canthp1  10640  mremre  17657  submre  17658  baspartn  23092  fctop  23142  cctop  23144  ppttop  23145  epttop  23147  isopn3  23204  mretopd  23230  tsmsfbas  24266  exsslsb  33965  gsumesum  34427  esumcst  34431  pwsiga  34498  prsiga  34499  sigainb  34504  pwldsys  34525  ldgenpisyslem1  34531  carsggect  34686  ex-sategoelel  35891  neibastop1  36848  neibastop2lem  36849  topdifinfindis  37970  elrfi  43405  dssmapnvod  44726  ntrk0kbimka  44745  clsk3nimkb  44746  neik0pk1imk0  44753  ntrclscls00  44772  ntrneicls00  44795  dvnprodlem3  46642  caragenunidm  47202