Theorem pwidg 4547

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3924  𝒫 cpw 4525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-in 3931  df-ss 3940  df-pw 4527

This theorem is referenced by:  pwidb  4548  pwid  4549  axpweq  5251  knatar  7096  brwdom2  9023  pwwf  9222  rankpwi  9238  canthp1lem2  10061  canthp1  10062  mremre  16858  submre  16859  baspartn  21545  fctop  21595  cctop  21597  ppttop  21598  epttop  21600  isopn3  21657  mretopd  21683  tsmsfbas  22719  gsumesum  31325  esumcst  31329  pwsiga  31396  prsiga  31397  sigainb  31402  pwldsys  31423  ldgenpisyslem1  31429  carsggect  31583  ex-sategoelel  32675  neibastop1  33714  neibastop2lem  33715  topdifinfindis  34643  elrfi  39383  dssmapnvod  40456  ntrk0kbimka  40479  clsk3nimkb  40480  neik0pk1imk0  40487  ntrclscls00  40506  ntrneicls00  40529  pwssfi  41397  dvnprodlem3  42323  caragenunidm  42880