Theorem pwidg 4576

Description: A set is an element of its power set. (Contributed by Stefan O'Rear, 1-Feb-2015.)

Assertion

Ref	Expression
pwidg	⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ 𝒫 𝐴)

Proof of Theorem pwidg

Step	Hyp	Ref	Expression
1		ssid 3958	. 2 ⊢ 𝐴 ⊆ 𝐴
2		elpwg 4559	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐴 ↔ 𝐴 ⊆ 𝐴))
3	1, 2	mpbiri 258	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ 𝒫 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3903  𝒫 cpw 4556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3920  df-pw 4558

This theorem is referenced by:  pwidb  4577  pwid  4578  axpweq  5298  knatar  7313  pwssfi  9113  brwdom2  9490  pwwf  9731  rankpwi  9747  canthp1lem2  10576  canthp1  10577  mremre  17535  submre  17536  baspartn  22910  fctop  22960  cctop  22962  ppttop  22963  epttop  22965  isopn3  23022  mretopd  23048  tsmsfbas  24084  exsslsb  33773  gsumesum  34236  esumcst  34240  pwsiga  34307  prsiga  34308  sigainb  34313  pwldsys  34334  ldgenpisyslem1  34340  carsggect  34495  ex-sategoelel  35634  neibastop1  36572  neibastop2lem  36573  topdifinfindis  37595  elrfi  43045  dssmapnvod  44370  ntrk0kbimka  44389  clsk3nimkb  44390  neik0pk1imk0  44397  ntrclscls00  44416  ntrneicls00  44439  dvnprodlem3  46300  caragenunidm  46860