Theorem pwidg 4570

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

Syntax hints:   → wi 4   ∈ wcel 2111   ⊆ wss 3902  𝒫 cpw 4550

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ss 3919  df-pw 4552

This theorem is referenced by:  pwidb  4571  pwid  4572  axpweq  5289  knatar  7291  pwssfi  9086  brwdom2  9459  pwwf  9697  rankpwi  9713  canthp1lem2  10541  canthp1  10542  mremre  17503  submre  17504  baspartn  22867  fctop  22917  cctop  22919  ppttop  22920  epttop  22922  isopn3  22979  mretopd  23005  tsmsfbas  24041  exsslsb  33604  gsumesum  34067  esumcst  34071  pwsiga  34138  prsiga  34139  sigainb  34144  pwldsys  34165  ldgenpisyslem1  34171  carsggect  34326  ex-sategoelel  35453  neibastop1  36392  neibastop2lem  36393  topdifinfindis  37379  elrfi  42726  dssmapnvod  44052  ntrk0kbimka  44071  clsk3nimkb  44072  neik0pk1imk0  44079  ntrclscls00  44098  ntrneicls00  44121  dvnprodlem3  45985  caragenunidm  46545