Theorem pwidg 4577

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3451  𝒫 cpw 4557

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-ss 3916  df-pw 4559

This theorem is used by:  pwidb  4579  pwid  4580  axpweq  5312  knatar  7359  pwssfi  9176  brwdom2  9551  pwwf  9797  rankpwi  9813  canthp1lem2  10719  canthp1  10720  mremre  17754  submre  17755  baspartn  23252  fctop  23302  cctop  23304  ppttop  23305  epttop  23307  isopn3  23364  mretopd  23390  tsmsfbas  24427  exsslsb  34211  gsumesum  34673  esumcst  34677  pwsiga  34744  prsiga  34745  sigainb  34751  pwldsys  34772  ldgenpisyslem1  34778  carsggect  34933  ex-sategoelel  36155  neibastop1  37117  neibastop2lem  37118  topdifinfindis  38237  elrfi  43658  dssmapnvod  44979  ntrk0kbimka  44998  clsk3nimkb  44999  neik0pk1imk0  45006  ntrclscls00  45025  ntrneicls00  45048  dvnprodlem3  46902  caragenunidm  47462  tmachlem-tpopen  47895