Theorem pwex 4774

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 4111	. . 3 ⊢ (𝑧 = 𝐴 → 𝒫 𝑧 = 𝒫 𝐴)
3	2	eleq1d 2672	. 2 ⊢ (𝑧 = 𝐴 → (𝒫 𝑧 ∈ V ↔ 𝒫 𝐴 ∈ V))
4		df-pw 4110	. . 3 ⊢ 𝒫 𝑧 = {𝑦 ∣ 𝑦 ⊆ 𝑧}
5		axpow2 4771	. . . . . 6 ⊢ ∃𝑥∀𝑦(𝑦 ⊆ 𝑧 → 𝑦 ∈ 𝑥)
6	5	bm1.3ii 4712	. . . . 5 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ⊆ 𝑧)
7		abeq2 2719	. . . . . 6 ⊢ (𝑥 = {𝑦 ∣ 𝑦 ⊆ 𝑧} ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ⊆ 𝑧))
8	7	exbii 1764	. . . . 5 ⊢ (∃𝑥 𝑥 = {𝑦 ∣ 𝑦 ⊆ 𝑧} ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ⊆ 𝑧))
9	6, 8	mpbir 220	. . . 4 ⊢ ∃𝑥 𝑥 = {𝑦 ∣ 𝑦 ⊆ 𝑧}
10	9	issetri 3183	. . 3 ⊢ {𝑦 ∣ 𝑦 ⊆ 𝑧} ∈ V
11	4, 10	eqeltri 2684	. 2 ⊢ 𝒫 𝑧 ∈ V
12	1, 3, 11	vtocl 3232	1 ⊢ 𝒫 𝐴 ∈ V

Syntax hints:   ↔ wb 195  ∀wal 1473   = wceq 1475  ∃wex 1695   ∈ wcel 1977  {cab 2596  Vcvv 3173   ⊆ wss 3540  𝒫 cpw 4108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-pow 4769

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-v 3175  df-in 3547  df-ss 3554  df-pw 4110

This theorem is referenced by:  vpwex  4775  p0ex  4779  pp0ex  4781  ord3ex  4782  abexssex  7041  fnpm  7752  canth2  7998  dffi3  8220  r1sucg  8515  r1pwALT  8592  rankuni  8609  rankc2  8617  rankxpu  8622  rankmapu  8624  rankxplim  8625  r0weon  8718  aceq3lem  8826  dfac5lem4  8832  dfac2a  8835  dfac2  8836  ackbij2lem2  8945  ackbij2lem3  8946  fin23lem17  9043  domtriomlem  9147  axdc2lem  9153  axdc3lem  9155  axdclem2  9225  alephsucpw  9271  canthp1lem1  9353  gchac  9382  gruina  9519  npex  9687  axcnex  9847  pnfxr  9971  mnfxr  9975  ixxex  12057  prdsval  15938  prdsds  15947  prdshom  15950  ismre  16073  fnmre  16074  fnmrc  16090  mrcfval  16091  mrisval  16113  wunfunc  16382  catcfuccl  16582  catcxpccl  16670  lubfval  16801  glbfval  16814  issubm  17170  issubg  17417  cntzfval  17576  sylow1lem2  17837  lsmfval  17876  pj1fval  17930  issubrg  18603  lssset  18755  lspfval  18794  islbs  18897  lbsext  18984  lbsexg  18985  sraval  18997  aspval  19149  ocvfval  19829  cssval  19845  isobs  19883  islinds  19967  istopon  20540  fncld  20636  leordtval2  20826  cnpfval  20848  iscnp2  20853  kgenf  21154  xkoopn  21202  xkouni  21212  dfac14  21231  xkoccn  21232  prdstopn  21241  xkoco1cn  21270  xkoco2cn  21271  xkococn  21273  xkoinjcn  21300  isfbas  21443  uzrest  21511  acufl  21531  alexsubALTlem2  21662  tsmsval2  21743  ustfn  21815  ustn0  21834  ishtpy  22579  vitali  23188  sspval  26962  shex  27453  hsupval  27577  fpwrelmap  28896  fpwrelmapffs  28897  isrnsigaOLD  29502  dmvlsiga  29519  eulerpartlem1  29756  eulerpartgbij  29761  eulerpartlemmf  29764  coinflippv  29872  ballotlemoex  29874  kur14lem9  30450  mpstval  30686  mclsrcl  30712  mclsval  30714  bj-dmtopon  32242  heibor1lem  32778  heibor  32790  idlval  32982  psubspset  34048  paddfval  34101  pclfvalN  34193  polfvalN  34208  psubclsetN  34240  docafvalN  35429  djafvalN  35441  dicval  35483  dochfval  35657  djhfval  35704  islpolN  35790  mzpclval  36306  eldiophb  36338  rpnnen3  36617  dfac11  36650  rgspnval  36757  clsk1independent  37364  dmvolsal  39240  ovnval  39431  smfresal  39673  issubmgm  41579  lincop  41991  setrec2fun  42238  vsetrec  42245  elpglem3  42255