Theorem pwidg 4519

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

Syntax hints:   → wi 4   ∈ wcel 2111   ⊆ wss 3881  𝒫 cpw 4497

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-pw 4499

This theorem is referenced by:  pwidb  4520  pwid  4521  axpweq  5230  knatar  7089  brwdom2  9021  pwwf  9220  rankpwi  9236  canthp1lem2  10064  canthp1  10065  mremre  16867  submre  16868  baspartn  21559  fctop  21609  cctop  21611  ppttop  21612  epttop  21614  isopn3  21671  mretopd  21697  tsmsfbas  22733  gsumesum  31428  esumcst  31432  pwsiga  31499  prsiga  31500  sigainb  31505  pwldsys  31526  ldgenpisyslem1  31532  carsggect  31686  ex-sategoelel  32781  neibastop1  33820  neibastop2lem  33821  topdifinfindis  34763  elrfi  39635  dssmapnvod  40721  ntrk0kbimka  40742  clsk3nimkb  40743  neik0pk1imk0  40750  ntrclscls00  40769  ntrneicls00  40792  pwssfi  41679  dvnprodlem3  42590  caragenunidm  43147