Theorem pwidg 4578

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

Syntax hints:   → wi 4   ∈ wcel 2145  Vcvv 3457  𝒫 cpw 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-ss 3924  df-pw 4560

This theorem is referenced by:  pwidb  4580  pwid  4581  axpweq  5312  knatar  7345  pwssfi  9149  brwdom2  9523  pwwf  9767  rankpwi  9783  canthp1lem2  10626  canthp1  10627  mremre  17646  submre  17647  baspartn  23072  fctop  23122  cctop  23124  ppttop  23125  epttop  23127  isopn3  23184  mretopd  23210  tsmsfbas  24246  exsslsb  33904  gsumesum  34366  esumcst  34370  pwsiga  34437  prsiga  34438  sigainb  34443  pwldsys  34464  ldgenpisyslem1  34470  carsggect  34625  ex-sategoelel  35784  neibastop1  36732  neibastop2lem  36733  topdifinfindis  37852  elrfi  43287  dssmapnvod  44608  ntrk0kbimka  44627  clsk3nimkb  44628  neik0pk1imk0  44635  ntrclscls00  44654  ntrneicls00  44677  dvnprodlem3  46520  caragenunidm  47080