Theorem pwidg 4552

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

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3883  𝒫 cpw 4530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-pw 4532

This theorem is referenced by:  pwidb  4553  pwid  4554  axpweq  5282  knatar  7208  brwdom2  9262  pwwf  9496  rankpwi  9512  canthp1lem2  10340  canthp1  10341  mremre  17230  submre  17231  baspartn  22012  fctop  22062  cctop  22064  ppttop  22065  epttop  22067  isopn3  22125  mretopd  22151  tsmsfbas  23187  gsumesum  31927  esumcst  31931  pwsiga  31998  prsiga  31999  sigainb  32004  pwldsys  32025  ldgenpisyslem1  32031  carsggect  32185  ex-sategoelel  33283  neibastop1  34475  neibastop2lem  34476  topdifinfindis  35444  elrfi  40432  dssmapnvod  41517  ntrk0kbimka  41538  clsk3nimkb  41539  neik0pk1imk0  41546  ntrclscls00  41565  ntrneicls00  41588  pwssfi  42482  dvnprodlem3  43379  caragenunidm  43936