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

Theorem pwexg 4036
Description: Power set axiom expressed in class notation, with the sethood requirement as an antecedent. (Contributed by NM, 30-Oct-2003.)
Assertion
Ref Expression
pwexg (𝐴𝑉 → 𝒫 𝐴 ∈ V)

Proof of Theorem pwexg
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 pweq 3452 . . 3 (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴)
21eleq1d 2163 . 2 (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V))
3 vpwex 4035 . 2 𝒫 𝑥 ∈ V
42, 3vtoclg 2693 1 (𝐴𝑉 → 𝒫 𝐴 ∈ V)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1296  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:  pwexd  4037  abssexg  4038  pwex  4039  snexg  4040  pwel  4069  uniexb  4323  xpexg  4581  fabexg  5233  mapex  6451  pmvalg  6456  fopwdom  6632  ssenen  6647  restid2  11829  toponsspwpwg  11888  tgdom  11940  distop  11953  epttop  11958  cldval  11967  ntrfval  11968  clsfval  11969  neifval  12008  neif  12009  neival  12011
  Copyright terms: Public domain W3C validator