Theorem pwidg 4519

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

Syntax hints:   → wi 4   ∈ wcel 2111   ⊆ wss 3860  𝒫 cpw 4497

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3867  df-ss 3877  df-pw 4499

This theorem is referenced by:  pwidb  4520  pwid  4521  axpweq  5236  knatar  7109  brwdom2  9075  pwwf  9274  rankpwi  9290  canthp1lem2  10118  canthp1  10119  mremre  16938  submre  16939  baspartn  21659  fctop  21709  cctop  21711  ppttop  21712  epttop  21714  isopn3  21771  mretopd  21797  tsmsfbas  22833  gsumesum  31550  esumcst  31554  pwsiga  31621  prsiga  31622  sigainb  31627  pwldsys  31648  ldgenpisyslem1  31654  carsggect  31808  ex-sategoelel  32903  neibastop1  34123  neibastop2lem  34124  topdifinfindis  35069  elrfi  40036  dssmapnvod  41122  ntrk0kbimka  41143  clsk3nimkb  41144  neik0pk1imk0  41151  ntrclscls00  41170  ntrneicls00  41193  pwssfi  42080  dvnprodlem3  42984  caragenunidm  43541