Theorem pwidg 4625

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

Syntax hints:   → wi 4   ∈ wcel 2106   ⊆ wss 3963  𝒫 cpw 4605

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ss 3980  df-pw 4607

This theorem is referenced by:  pwidb  4626  pwid  4627  axpweq  5357  knatar  7377  brwdom2  9611  pwwf  9845  rankpwi  9861  canthp1lem2  10691  canthp1  10692  mremre  17649  submre  17650  baspartn  22977  fctop  23027  cctop  23029  ppttop  23030  epttop  23032  isopn3  23090  mretopd  23116  tsmsfbas  24152  gsumesum  34040  esumcst  34044  pwsiga  34111  prsiga  34112  sigainb  34117  pwldsys  34138  ldgenpisyslem1  34144  carsggect  34300  ex-sategoelel  35406  neibastop1  36342  neibastop2lem  36343  topdifinfindis  37329  elrfi  42682  dssmapnvod  44010  ntrk0kbimka  44029  clsk3nimkb  44030  neik0pk1imk0  44037  ntrclscls00  44056  ntrneicls00  44079  pwssfi  44985  dvnprodlem3  45904  caragenunidm  46464