Theorem pwidg 4600

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3931  𝒫 cpw 4580

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ss 3948  df-pw 4582

This theorem is referenced by:  pwidb  4601  pwid  4602  axpweq  5326  knatar  7355  pwssfi  9196  brwdom2  9592  pwwf  9826  rankpwi  9842  canthp1lem2  10672  canthp1  10673  mremre  17621  submre  17622  baspartn  22897  fctop  22947  cctop  22949  ppttop  22950  epttop  22952  isopn3  23009  mretopd  23035  tsmsfbas  24071  exsslsb  33641  gsumesum  34095  esumcst  34099  pwsiga  34166  prsiga  34167  sigainb  34172  pwldsys  34193  ldgenpisyslem1  34199  carsggect  34355  ex-sategoelel  35448  neibastop1  36382  neibastop2lem  36383  topdifinfindis  37369  elrfi  42684  dssmapnvod  44011  ntrk0kbimka  44030  clsk3nimkb  44031  neik0pk1imk0  44038  ntrclscls00  44057  ntrneicls00  44080  dvnprodlem3  45944  caragenunidm  46504