Theorem pwidg 4562

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3890  𝒫 cpw 4542

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 3907  df-pw 4544

This theorem is referenced by:  pwidb  4563  pwid  4564  axpweq  5286  knatar  7303  pwssfi  9102  brwdom2  9479  pwwf  9720  rankpwi  9736  canthp1lem2  10565  canthp1  10566  mremre  17555  submre  17556  baspartn  22928  fctop  22978  cctop  22980  ppttop  22981  epttop  22983  isopn3  23040  mretopd  23066  tsmsfbas  24102  exsslsb  33761  gsumesum  34224  esumcst  34228  pwsiga  34295  prsiga  34296  sigainb  34301  pwldsys  34322  ldgenpisyslem1  34328  carsggect  34483  ex-sategoelel  35624  neibastop1  36562  neibastop2lem  36563  topdifinfindis  37673  elrfi  43137  dssmapnvod  44462  ntrk0kbimka  44481  clsk3nimkb  44482  neik0pk1imk0  44489  ntrclscls00  44508  ntrneicls00  44531  dvnprodlem3  46391  caragenunidm  46951