Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  pwex GIF version

Theorem pwex 4039
 Description: Power set axiom expressed in class notation. (Contributed by NM, 21-Jun-1993.)
Hypothesis
Ref Expression
pwex.1 𝐴 ∈ V
Assertion
Ref Expression
pwex 𝒫 𝐴 ∈ V

Proof of Theorem pwex
StepHypRef Expression
1 pwex.1 . 2 𝐴 ∈ V
2 pwexg 4036 . 2 (𝐴 ∈ V → 𝒫 𝐴 ∈ V)
31, 2ax-mp 7 1 𝒫 𝐴 ∈ V
 Colors of variables: wff set class Syntax hints:   ∈ wcel 1445  Vcvv 2633  𝒫 cpw 3449 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-14 1457  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077  ax-sep 3978  ax-pow 4030 This theorem depends on definitions:  df-bi 116  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-v 2635  df-in 3019  df-ss 3026  df-pw 3451 This theorem is referenced by:  p0ex  4044  pp0ex  4045  ord3ex  4046  abexssex  5934  fnpm  6453  exmidpw  6704  npex  7129  axcnex  7493  pnfxr  7637  mnfxr  7641  ixxex  9465  istopon  11864  dmtopon  11873  fncld  11950  pw1dom2  12595
 Copyright terms: Public domain W3C validator