Theorem pwidg 4561

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3889  𝒫 cpw 4541

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ss 3906  df-pw 4543

This theorem is referenced by:  pwidb  4562  pwid  4563  axpweq  5292  knatar  7312  pwssfi  9111  brwdom2  9488  pwwf  9731  rankpwi  9747  canthp1lem2  10576  canthp1  10577  mremre  17566  submre  17567  baspartn  22919  fctop  22969  cctop  22971  ppttop  22972  epttop  22974  isopn3  23031  mretopd  23057  tsmsfbas  24093  exsslsb  33741  gsumesum  34203  esumcst  34207  pwsiga  34274  prsiga  34275  sigainb  34280  pwldsys  34301  ldgenpisyslem1  34307  carsggect  34462  ex-sategoelel  35603  neibastop1  36541  neibastop2lem  36542  topdifinfindis  37662  elrfi  43126  dssmapnvod  44447  ntrk0kbimka  44466  clsk3nimkb  44467  neik0pk1imk0  44474  ntrclscls00  44493  ntrneicls00  44516  dvnprodlem3  46376  caragenunidm  46936