Theorem pwidg 4580

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 3957	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ 𝐴)
3	1, 2	elpwd 4566	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ 𝒫 𝐴)

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

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 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-ss 3919  df-pw 4562

This theorem is used by:  pwidb  4582  pwid  4583  axpweq  5319  knatar  7364  pwssfi  9175  brwdom2  9549  pwwf  9793  rankpwi  9809  canthp1lem2  10666  canthp1  10667  mremre  17694  submre  17695  baspartn  23185  fctop  23235  cctop  23237  ppttop  23238  epttop  23240  isopn3  23297  mretopd  23323  tsmsfbas  24360  exsslsb  34115  gsumesum  34577  esumcst  34581  pwsiga  34648  prsiga  34649  sigainb  34655  pwldsys  34676  ldgenpisyslem1  34682  carsggect  34837  ex-sategoelel  36008  neibastop1  36986  neibastop2lem  36987  topdifinfindis  38108  elrfi  43547  dssmapnvod  44868  ntrk0kbimka  44887  clsk3nimkb  44888  neik0pk1imk0  44895  ntrclscls00  44914  ntrneicls00  44937  dvnprodlem3  46784  caragenunidm  47344  tmachlem-tpopen  47777