Theorem pwidg 4586

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 3972	. 2 ⊢ 𝐴 ⊆ 𝐴
2		elpwg 4569	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐴 ↔ 𝐴 ⊆ 𝐴))
3	1, 2	mpbiri 258	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ 𝒫 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3917  𝒫 cpw 4566

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ss 3934  df-pw 4568

This theorem is referenced by:  pwidb  4587  pwid  4588  axpweq  5309  knatar  7335  pwssfi  9147  brwdom2  9533  pwwf  9767  rankpwi  9783  canthp1lem2  10613  canthp1  10614  mremre  17572  submre  17573  baspartn  22848  fctop  22898  cctop  22900  ppttop  22901  epttop  22903  isopn3  22960  mretopd  22986  tsmsfbas  24022  exsslsb  33599  gsumesum  34056  esumcst  34060  pwsiga  34127  prsiga  34128  sigainb  34133  pwldsys  34154  ldgenpisyslem1  34160  carsggect  34316  ex-sategoelel  35415  neibastop1  36354  neibastop2lem  36355  topdifinfindis  37341  elrfi  42689  dssmapnvod  44016  ntrk0kbimka  44035  clsk3nimkb  44036  neik0pk1imk0  44043  ntrclscls00  44062  ntrneicls00  44085  dvnprodlem3  45953  caragenunidm  46513