Theorem pwidg 4583

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3914  𝒫 cpw 4563

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 3931  df-pw 4565

This theorem is referenced by:  pwidb  4584  pwid  4585  axpweq  5306  knatar  7332  pwssfi  9141  brwdom2  9526  pwwf  9760  rankpwi  9776  canthp1lem2  10606  canthp1  10607  mremre  17565  submre  17566  baspartn  22841  fctop  22891  cctop  22893  ppttop  22894  epttop  22896  isopn3  22953  mretopd  22979  tsmsfbas  24015  exsslsb  33592  gsumesum  34049  esumcst  34053  pwsiga  34120  prsiga  34121  sigainb  34126  pwldsys  34147  ldgenpisyslem1  34153  carsggect  34309  ex-sategoelel  35408  neibastop1  36347  neibastop2lem  36348  topdifinfindis  37334  elrfi  42682  dssmapnvod  44009  ntrk0kbimka  44028  clsk3nimkb  44029  neik0pk1imk0  44036  ntrclscls00  44055  ntrneicls00  44078  dvnprodlem3  45946  caragenunidm  46506