Theorem pwidg 4587

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  Vcvv 3458  𝒫 cpw 4567

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-ss 3925  df-pw 4569

This theorem is used by:  pwidb  4589  pwid  4590  axpweq  5326  knatar  7368  pwssfi  9171  brwdom2  9545  pwwf  9789  rankpwi  9805  canthp1lem2  10656  canthp1  10657  mremre  17681  submre  17682  baspartn  23148  fctop  23198  cctop  23200  ppttop  23201  epttop  23203  isopn3  23260  mretopd  23286  tsmsfbas  24322  exsslsb  34018  gsumesum  34480  esumcst  34484  pwsiga  34551  prsiga  34552  sigainb  34558  pwldsys  34579  ldgenpisyslem1  34585  carsggect  34740  ex-sategoelel  35934  neibastop1  36911  neibastop2lem  36912  topdifinfindis  38033  elrfi  43466  dssmapnvod  44787  ntrk0kbimka  44806  clsk3nimkb  44807  neik0pk1imk0  44814  ntrclscls00  44833  ntrneicls00  44856  dvnprodlem3  46703  caragenunidm  47263