Theorem pwidg 4622

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

Syntax hints:   → wi 4   ∈ wcel 2106   ⊆ wss 3948  𝒫 cpw 4602

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965  df-pw 4604

This theorem is referenced by:  pwidb  4623  pwid  4624  axpweq  5348  knatar  7353  brwdom2  9567  pwwf  9801  rankpwi  9817  canthp1lem2  10647  canthp1  10648  mremre  17547  submre  17548  baspartn  22456  fctop  22506  cctop  22508  ppttop  22509  epttop  22511  isopn3  22569  mretopd  22595  tsmsfbas  23631  gsumesum  33052  esumcst  33056  pwsiga  33123  prsiga  33124  sigainb  33129  pwldsys  33150  ldgenpisyslem1  33156  carsggect  33312  ex-sategoelel  34407  neibastop1  35239  neibastop2lem  35240  topdifinfindis  36222  elrfi  41422  dssmapnvod  42761  ntrk0kbimka  42780  clsk3nimkb  42781  neik0pk1imk0  42788  ntrclscls00  42807  ntrneicls00  42830  pwssfi  43722  dvnprodlem3  44654  caragenunidm  45214