Theorem pwidg 4574

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

Syntax hints:   → wi 4   ∈ wcel 2141  Vcvv 3453  𝒫 cpw 4554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-ss 3921  df-pw 4556

This theorem is referenced by:  pwidb  4576  pwid  4577  axpweq  5306  knatar  7337  pwssfi  9141  brwdom2  9518  pwwf  9762  rankpwi  9778  canthp1lem2  10608  canthp1  10609  mremre  17615  submre  17616  baspartn  22994  fctop  23044  cctop  23046  ppttop  23047  epttop  23049  isopn3  23106  mretopd  23132  tsmsfbas  24168  exsslsb  33855  gsumesum  34317  esumcst  34321  pwsiga  34388  prsiga  34389  sigainb  34394  pwldsys  34415  ldgenpisyslem1  34421  carsggect  34576  ex-sategoelel  35735  neibastop1  36683  neibastop2lem  36684  topdifinfindis  37804  elrfi  43239  dssmapnvod  44560  ntrk0kbimka  44579  clsk3nimkb  44580  neik0pk1imk0  44587  ntrclscls00  44606  ntrneicls00  44629  dvnprodlem3  46486  caragenunidm  47046