Theorem pwex 4839

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.

Step	Hyp	Ref	Expression
1		zfpowcl.1	. 2 ⊢ 𝐴 ∈ V
2		pweq 4152	. . 3 ⊢ (𝑧 = 𝐴 → 𝒫 𝑧 = 𝒫 𝐴)
3	2	eleq1d 2684	. 2 ⊢ (𝑧 = 𝐴 → (𝒫 𝑧 ∈ V ↔ 𝒫 𝐴 ∈ V))
4		df-pw 4151	. . 3 ⊢ 𝒫 𝑧 = {𝑦 ∣ 𝑦 ⊆ 𝑧}
5		axpow2 4836	. . . . . 6 ⊢ ∃𝑥∀𝑦(𝑦 ⊆ 𝑧 → 𝑦 ∈ 𝑥)
6	5	bm1.3ii 4775	. . . . 5 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ⊆ 𝑧)
7		abeq2 2730	. . . . . 6 ⊢ (𝑥 = {𝑦 ∣ 𝑦 ⊆ 𝑧} ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ⊆ 𝑧))
8	7	exbii 1772	. . . . 5 ⊢ (∃𝑥 𝑥 = {𝑦 ∣ 𝑦 ⊆ 𝑧} ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ⊆ 𝑧))
9	6, 8	mpbir 221	. . . 4 ⊢ ∃𝑥 𝑥 = {𝑦 ∣ 𝑦 ⊆ 𝑧}
10	9	issetri 3205	. . 3 ⊢ {𝑦 ∣ 𝑦 ⊆ 𝑧} ∈ V
11	4, 10	eqeltri 2695	. 2 ⊢ 𝒫 𝑧 ∈ V
12	1, 3, 11	vtocl 3254	1 ⊢ 𝒫 𝐴 ∈ V

Syntax hints:   ↔ wb 196  ∀wal 1479   = wceq 1481  ∃wex 1702   ∈ wcel 1988  {cab 2606  Vcvv 3195   ⊆ wss 3567  𝒫 cpw 4149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-pow 4834

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-v 3197  df-in 3574  df-ss 3581  df-pw 4151

This theorem is referenced by:  vpwex  4840  p0ex  4844  pp0ex  4846  ord3ex  4847  abexssex  7134  fnpm  7850  canth2  8098  dffi3  8322  r1sucg  8617  r1pwALT  8694  rankuni  8711  rankc2  8719  rankxpu  8724  rankmapu  8726  rankxplim  8727  r0weon  8820  aceq3lem  8928  dfac5lem4  8934  dfac2a  8937  dfac2  8938  ackbij2lem2  9047  ackbij2lem3  9048  fin23lem17  9145  domtriomlem  9249  axdc2lem  9255  axdc3lem  9257  axdclem2  9327  alephsucpw  9377  canthp1lem1  9459  gchac  9488  gruina  9625  npex  9793  axcnex  9953  pnfxr  10077  mnfxr  10081  ixxex  12171  prdsval  16096  prdsds  16105  prdshom  16108  ismre  16231  fnmre  16232  fnmrc  16248  mrcfval  16249  mrisval  16271  wunfunc  16540  catcfuccl  16740  catcxpccl  16828  lubfval  16959  glbfval  16972  issubm  17328  issubg  17575  cntzfval  17734  sylow1lem2  17995  lsmfval  18034  pj1fval  18088  issubrg  18761  lssset  18915  lspfval  18954  islbs  19057  lbsext  19144  lbsexg  19145  sraval  19157  aspval  19309  ocvfval  19991  cssval  20007  isobs  20045  islinds  20129  istopon  20698  dmtopon  20708  fncld  20807  leordtval2  20997  cnpfval  21019  iscnp2  21024  kgenf  21325  xkoopn  21373  xkouni  21383  dfac14  21402  xkoccn  21403  prdstopn  21412  xkoco1cn  21441  xkoco2cn  21442  xkococn  21444  xkoinjcn  21471  isfbas  21614  uzrest  21682  acufl  21702  alexsubALTlem2  21833  tsmsval2  21914  ustfn  21986  ustn0  22005  ishtpy  22752  vitali  23363  sspval  27548  shex  28039  hsupval  28163  fpwrelmap  29482  fpwrelmapffs  29483  isrnsigaOLD  30149  dmvlsiga  30166  eulerpartlem1  30403  eulerpartgbij  30408  eulerpartlemmf  30411  coinflippv  30519  ballotlemoex  30521  reprval  30662  kur14lem9  31170  mpstval  31406  mclsrcl  31432  mclsval  31434  heibor1lem  33579  heibor  33591  idlval  33783  psubspset  34849  paddfval  34902  pclfvalN  34994  polfvalN  35009  psubclsetN  35041  docafvalN  36230  djafvalN  36242  dicval  36284  dochfval  36458  djhfval  36505  islpolN  36591  mzpclval  37107  eldiophb  37139  rpnnen3  37418  dfac11  37451  rgspnval  37557  clsk1independent  38164  dmvolsal  40327  ovnval  40518  smfresal  40758  sprbisymrel  41514  uspgrex  41523  uspgrbisymrelALT  41528  issubmgm  41554  lincop  41962  setrec2fun  42204  vsetrec  42211  elpglem3  42221