Theorem pwidg 4394

Description: Membership of the original in a power set. (Contributed by Stefan O'Rear, 1-Feb-2015.)

Assertion

Ref	Expression
pwidg	⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ 𝒫 𝐴)

Proof of Theorem pwidg

Step	Hyp	Ref	Expression
1		ssid 3849	. 2 ⊢ 𝐴 ⊆ 𝐴
2		elpwg 4387	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝐴 ↔ 𝐴 ⊆ 𝐴))
3	1, 2	mpbiri 250	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ 𝒫 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2166   ⊆ wss 3799  𝒫 cpw 4379

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2804

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-v 3417  df-in 3806  df-ss 3813  df-pw 4381

This theorem is referenced by:  pwid  4395  axpweq  5065  knatar  6863  brwdom2  8748  pwwf  8948  rankpwi  8964  canthp1lem2  9791  canthp1  9792  grothpw  9964  mremre  16618  submre  16619  baspartn  21130  fctop  21180  cctop  21182  ppttop  21183  epttop  21185  isopn3  21242  mretopd  21268  tsmsfbas  22302  gsumesum  30667  esumcst  30671  pwsiga  30739  prsiga  30740  sigainb  30745  pwldsys  30766  ldgenpisyslem1  30772  carsggect  30926  neibastop1  32893  neibastop2lem  32894  topdifinfindis  33740  elrfi  38102  dssmapnvod  39155  ntrk0kbimka  39178  clsk3nimkb  39179  neik0pk1imk0  39186  ntrclscls00  39205  ntrneicls00  39228  pwssfi  40029  dvnprodlem3  40959  caragenunidm  41517