Theorem pwidg 4619

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

Syntax hints:   → wi 4   ∈ wcel 2107   ⊆ wss 3950  𝒫 cpw 4599

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ss 3967  df-pw 4601

This theorem is referenced by:  pwidb  4620  pwid  4621  axpweq  5350  knatar  7378  pwssfi  9218  brwdom2  9614  pwwf  9848  rankpwi  9864  canthp1lem2  10694  canthp1  10695  mremre  17648  submre  17649  baspartn  22962  fctop  23012  cctop  23014  ppttop  23015  epttop  23017  isopn3  23075  mretopd  23101  tsmsfbas  24137  exsslsb  33648  gsumesum  34061  esumcst  34065  pwsiga  34132  prsiga  34133  sigainb  34138  pwldsys  34159  ldgenpisyslem1  34165  carsggect  34321  ex-sategoelel  35427  neibastop1  36361  neibastop2lem  36362  topdifinfindis  37348  elrfi  42710  dssmapnvod  44038  ntrk0kbimka  44057  clsk3nimkb  44058  neik0pk1imk0  44065  ntrclscls00  44084  ntrneicls00  44107  dvnprodlem3  45968  caragenunidm  46528