Theorem pwidg 4574

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

Syntax hints:   → wi 4   ∈ wcel 2113   ⊆ wss 3901  𝒫 cpw 4554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ss 3918  df-pw 4556

This theorem is referenced by:  pwidb  4575  pwid  4576  axpweq  5296  knatar  7303  pwssfi  9101  brwdom2  9478  pwwf  9719  rankpwi  9735  canthp1lem2  10564  canthp1  10565  mremre  17523  submre  17524  baspartn  22898  fctop  22948  cctop  22950  ppttop  22951  epttop  22953  isopn3  23010  mretopd  23036  tsmsfbas  24072  exsslsb  33753  gsumesum  34216  esumcst  34220  pwsiga  34287  prsiga  34288  sigainb  34293  pwldsys  34314  ldgenpisyslem1  34320  carsggect  34475  ex-sategoelel  35615  neibastop1  36553  neibastop2lem  36554  topdifinfindis  37547  elrfi  42932  dssmapnvod  44257  ntrk0kbimka  44276  clsk3nimkb  44277  neik0pk1imk0  44284  ntrclscls00  44303  ntrneicls00  44326  dvnprodlem3  46188  caragenunidm  46748