Theorem pwidg 4562

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3890  𝒫 cpw 4542

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3907  df-pw 4544

This theorem is referenced by:  pwidb  4563  pwid  4564  axpweq  5288  knatar  7305  pwssfi  9104  brwdom2  9481  pwwf  9722  rankpwi  9738  canthp1lem2  10567  canthp1  10568  mremre  17557  submre  17558  baspartn  22929  fctop  22979  cctop  22981  ppttop  22982  epttop  22984  isopn3  23041  mretopd  23067  tsmsfbas  24103  exsslsb  33756  gsumesum  34219  esumcst  34223  pwsiga  34290  prsiga  34291  sigainb  34296  pwldsys  34317  ldgenpisyslem1  34323  carsggect  34478  ex-sategoelel  35619  neibastop1  36557  neibastop2lem  36558  topdifinfindis  37676  elrfi  43140  dssmapnvod  44465  ntrk0kbimka  44484  clsk3nimkb  44485  neik0pk1imk0  44492  ntrclscls00  44511  ntrneicls00  44534  dvnprodlem3  46394  caragenunidm  46954