Theorem pwidg 4556

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

Syntax hints:   → wi 4   ∈ wcel 2107   ⊆ wss 3888  𝒫 cpw 4534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905  df-pw 4536

This theorem is referenced by:  pwidb  4557  pwid  4558  axpweq  5288  knatar  7237  brwdom2  9341  pwwf  9574  rankpwi  9590  canthp1lem2  10418  canthp1  10419  mremre  17322  submre  17323  baspartn  22113  fctop  22163  cctop  22165  ppttop  22166  epttop  22168  isopn3  22226  mretopd  22252  tsmsfbas  23288  gsumesum  32036  esumcst  32040  pwsiga  32107  prsiga  32108  sigainb  32113  pwldsys  32134  ldgenpisyslem1  32140  carsggect  32294  ex-sategoelel  33392  neibastop1  34557  neibastop2lem  34558  topdifinfindis  35526  elrfi  40523  dssmapnvod  41635  ntrk0kbimka  41656  clsk3nimkb  41657  neik0pk1imk0  41664  ntrclscls00  41683  ntrneicls00  41706  pwssfi  42600  dvnprodlem3  43496  caragenunidm  44053