Theorem pwidg 4563

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3938  𝒫 cpw 4541

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-in 3945  df-ss 3954  df-pw 4543

This theorem is referenced by:  pwidb  4564  pwid  4565  axpweq  5267  knatar  7112  brwdom2  9039  pwwf  9238  rankpwi  9254  canthp1lem2  10077  canthp1  10078  mremre  16877  submre  16878  baspartn  21564  fctop  21614  cctop  21616  ppttop  21617  epttop  21619  isopn3  21676  mretopd  21702  tsmsfbas  22738  gsumesum  31320  esumcst  31324  pwsiga  31391  prsiga  31392  sigainb  31397  pwldsys  31418  ldgenpisyslem1  31424  carsggect  31578  ex-sategoelel  32670  neibastop1  33709  neibastop2lem  33710  topdifinfindis  34629  elrfi  39298  dssmapnvod  40373  ntrk0kbimka  40396  clsk3nimkb  40397  neik0pk1imk0  40404  ntrclscls00  40423  ntrneicls00  40446  pwssfi  41314  dvnprodlem3  42240  caragenunidm  42797