Theorem pwidg 4573

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3905  𝒫 cpw 4553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3922  df-pw 4555

This theorem is referenced by:  pwidb  4574  pwid  4575  axpweq  5293  knatar  7298  pwssfi  9101  brwdom2  9484  pwwf  9722  rankpwi  9738  canthp1lem2  10566  canthp1  10567  mremre  17524  submre  17525  baspartn  22857  fctop  22907  cctop  22909  ppttop  22910  epttop  22912  isopn3  22969  mretopd  22995  tsmsfbas  24031  exsslsb  33568  gsumesum  34025  esumcst  34029  pwsiga  34096  prsiga  34097  sigainb  34102  pwldsys  34123  ldgenpisyslem1  34129  carsggect  34285  ex-sategoelel  35393  neibastop1  36332  neibastop2lem  36333  topdifinfindis  37319  elrfi  42667  dssmapnvod  43993  ntrk0kbimka  44012  clsk3nimkb  44013  neik0pk1imk0  44020  ntrclscls00  44039  ntrneicls00  44062  dvnprodlem3  45930  caragenunidm  46490