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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Vcvv 3450  𝒫 cpw 4556

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-pw 4558

This theorem is used by:  pwidb  4579  pwid  4580  axpweq  5311  knatar  7367  pwssfi  9195  brwdom2  9570  pwwf  9818  rankpwi  9835  canthp1lem2  10741  canthp1  10742  mremre  17779  submre  17780  baspartn  23277  fctop  23327  cctop  23329  ppttop  23330  epttop  23332  isopn3  23389  mretopd  23415  tsmsfbas  24452  exsslsb  34275  gsumesum  34737  esumcst  34741  pwsiga  34808  prsiga  34809  sigainb  34815  pwldsys  34836  ldgenpisyslem1  34842  carsggect  34996  ex-sategoelel  36272  neibastop1  37239  neibastop2lem  37240  topdifinfindis  38362  elrfi  43798  dssmapnvod  45113  ntrk0kbimka  45132  clsk3nimkb  45133  neik0pk1imk0  45140  ntrclscls00  45159  ntrneicls00  45182  dvnprodlem3  47051  caragenunidm  47611  tmachlem-tpopen  48044