Theorem pwidg 4642

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

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3976  𝒫 cpw 4622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ss 3993  df-pw 4624

This theorem is referenced by:  pwidb  4643  pwid  4644  axpweq  5369  knatar  7393  brwdom2  9642  pwwf  9876  rankpwi  9892  canthp1lem2  10722  canthp1  10723  mremre  17662  submre  17663  baspartn  22982  fctop  23032  cctop  23034  ppttop  23035  epttop  23037  isopn3  23095  mretopd  23121  tsmsfbas  24157  gsumesum  34023  esumcst  34027  pwsiga  34094  prsiga  34095  sigainb  34100  pwldsys  34121  ldgenpisyslem1  34127  carsggect  34283  ex-sategoelel  35389  neibastop1  36325  neibastop2lem  36326  topdifinfindis  37312  elrfi  42650  dssmapnvod  43982  ntrk0kbimka  44001  clsk3nimkb  44002  neik0pk1imk0  44009  ntrclscls00  44028  ntrneicls00  44051  pwssfi  44947  dvnprodlem3  45869  caragenunidm  46429