MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pwex Structured version   Visualization version   GIF version

Theorem pwex 4878
Description: Power set axiom expressed in class notation. Axiom 4 of [TakeutiZaring] p. 17. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
Hypothesis
Ref Expression
zfpowcl.1 𝐴 ∈ V
Assertion
Ref Expression
pwex 𝒫 𝐴 ∈ V

Proof of Theorem pwex
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 zfpowcl.1 . 2 𝐴 ∈ V
2 pweq 4194 . . 3 (𝑧 = 𝐴 → 𝒫 𝑧 = 𝒫 𝐴)
32eleq1d 2715 . 2 (𝑧 = 𝐴 → (𝒫 𝑧 ∈ V ↔ 𝒫 𝐴 ∈ V))
4 df-pw 4193 . . 3 𝒫 𝑧 = {𝑦𝑦𝑧}
5 axpow2 4875 . . . . . 6 𝑥𝑦(𝑦𝑧𝑦𝑥)
65bm1.3ii 4817 . . . . 5 𝑥𝑦(𝑦𝑥𝑦𝑧)
7 abeq2 2761 . . . . . 6 (𝑥 = {𝑦𝑦𝑧} ↔ ∀𝑦(𝑦𝑥𝑦𝑧))
87exbii 1814 . . . . 5 (∃𝑥 𝑥 = {𝑦𝑦𝑧} ↔ ∃𝑥𝑦(𝑦𝑥𝑦𝑧))
96, 8mpbir 221 . . . 4 𝑥 𝑥 = {𝑦𝑦𝑧}
109issetri 3241 . . 3 {𝑦𝑦𝑧} ∈ V
114, 10eqeltri 2726 . 2 𝒫 𝑧 ∈ V
121, 3, 11vtocl 3290 1 𝒫 𝐴 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wb 196  wal 1521   = wceq 1523  wex 1744  wcel 2030  {cab 2637  Vcvv 3231  wss 3607  𝒫 cpw 4191
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-pow 4873
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-v 3233  df-in 3614  df-ss 3621  df-pw 4193
This theorem is referenced by:  vpwex  4879  p0ex  4883  pp0ex  4885  ord3ex  4886  abexssex  7191  fnpm  7907  canth2  8154  dffi3  8378  r1sucg  8670  r1pwALT  8747  rankuni  8764  rankc2  8772  rankxpu  8777  rankmapu  8779  rankxplim  8780  r0weon  8873  aceq3lem  8981  dfac5lem4  8987  dfac2a  8990  dfac2  8991  ackbij2lem2  9100  ackbij2lem3  9101  fin23lem17  9198  domtriomlem  9302  axdc2lem  9308  axdc3lem  9310  axdclem2  9380  alephsucpw  9430  canthp1lem1  9512  gchac  9541  gruina  9678  npex  9846  axcnex  10006  pnfxr  10130  mnfxr  10134  ixxex  12224  prdsval  16162  prdsds  16171  prdshom  16174  ismre  16297  fnmre  16298  fnmrc  16314  mrcfval  16315  mrisval  16337  wunfunc  16606  catcfuccl  16806  catcxpccl  16894  lubfval  17025  glbfval  17038  issubm  17394  issubg  17641  cntzfval  17799  sylow1lem2  18060  lsmfval  18099  pj1fval  18153  issubrg  18828  lssset  18982  lspfval  19021  islbs  19124  lbsext  19211  lbsexg  19212  sraval  19224  aspval  19376  ocvfval  20058  cssval  20074  isobs  20112  islinds  20196  istopon  20765  dmtopon  20775  fncld  20874  leordtval2  21064  cnpfval  21086  iscnp2  21091  kgenf  21392  xkoopn  21440  xkouni  21450  dfac14  21469  xkoccn  21470  prdstopn  21479  xkoco1cn  21508  xkoco2cn  21509  xkococn  21511  xkoinjcn  21538  isfbas  21680  uzrest  21748  acufl  21768  alexsubALTlem2  21899  tsmsval2  21980  ustfn  22052  ustn0  22071  ishtpy  22818  vitali  23427  sspval  27706  shex  28197  hsupval  28321  fpwrelmap  29636  fpwrelmapffs  29637  isrnsigaOLD  30303  dmvlsiga  30320  eulerpartlem1  30557  eulerpartgbij  30562  eulerpartlemmf  30565  coinflippv  30673  ballotlemoex  30675  reprval  30816  kur14lem9  31322  mpstval  31558  mclsrcl  31584  mclsval  31586  heibor1lem  33738  heibor  33750  idlval  33942  psubspset  35348  paddfval  35401  pclfvalN  35493  polfvalN  35508  psubclsetN  35540  docafvalN  36728  djafvalN  36740  dicval  36782  dochfval  36956  djhfval  37003  islpolN  37089  mzpclval  37605  eldiophb  37637  rpnnen3  37916  dfac11  37949  rgspnval  38055  clsk1independent  38661  dmvolsal  40882  ovnval  41076  smfresal  41316  sprbisymrel  42074  uspgrex  42083  uspgrbisymrelALT  42088  issubmgm  42114  lincop  42522  setrec2fun  42764  vsetrec  42774  elpglem3  42784
  Copyright terms: Public domain W3C validator