Theorem pwidg 4556

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

Syntax hints:   → wi 4   ∈ wcel 2119   ⊆ wss 3890  𝒫 cpw 4536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ss 3907  df-pw 4538

This theorem is referenced by:  pwidb  4557  pwid  4558  axpweq  5286  knatar  7308  pwssfi  9108  brwdom2  9485  pwwf  9729  rankpwi  9745  canthp1lem2  10574  canthp1  10575  mremre  17564  submre  17565  baspartn  22944  fctop  22994  cctop  22996  ppttop  22997  epttop  22999  isopn3  23056  mretopd  23082  tsmsfbas  24118  exsslsb  33788  gsumesum  34250  esumcst  34254  pwsiga  34321  prsiga  34322  sigainb  34327  pwldsys  34348  ldgenpisyslem1  34354  carsggect  34509  ex-sategoelel  35656  neibastop1  36594  neibastop2lem  36595  topdifinfindis  37715  elrfi  43150  dssmapnvod  44471  ntrk0kbimka  44490  clsk3nimkb  44491  neik0pk1imk0  44498  ntrclscls00  44517  ntrneicls00  44540  dvnprodlem3  46398  caragenunidm  46958