Theorem pwidg 4569

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

Syntax hints:   → wi 4   ∈ wcel 2113   ⊆ wss 3898  𝒫 cpw 4549

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ss 3915  df-pw 4551

This theorem is referenced by:  pwidb  4570  pwid  4571  axpweq  5291  knatar  7297  pwssfi  9093  brwdom2  9466  pwwf  9707  rankpwi  9723  canthp1lem2  10551  canthp1  10552  mremre  17508  submre  17509  baspartn  22870  fctop  22920  cctop  22922  ppttop  22923  epttop  22925  isopn3  22982  mretopd  23008  tsmsfbas  24044  exsslsb  33630  gsumesum  34093  esumcst  34097  pwsiga  34164  prsiga  34165  sigainb  34170  pwldsys  34191  ldgenpisyslem1  34197  carsggect  34352  ex-sategoelel  35486  neibastop1  36424  neibastop2lem  36425  topdifinfindis  37411  elrfi  42811  dssmapnvod  44137  ntrk0kbimka  44156  clsk3nimkb  44157  neik0pk1imk0  44164  ntrclscls00  44183  ntrneicls00  44206  dvnprodlem3  46070  caragenunidm  46630