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.

Step	Hyp	Ref	Expression
1		zfpowcl.1	. 2 ⊢ 𝐴 ∈ V
2		pweq 4194	. . 3 ⊢ (𝑧 = 𝐴 → 𝒫 𝑧 = 𝒫 𝐴)
3	2	eleq1d 2715	. 2 ⊢ (𝑧 = 𝐴 → (𝒫 𝑧 ∈ V ↔ 𝒫 𝐴 ∈ V))
4		df-pw 4193	. . 3 ⊢ 𝒫 𝑧 = {𝑦 ∣ 𝑦 ⊆ 𝑧}
5		axpow2 4875	. . . . . 6 ⊢ ∃𝑥∀𝑦(𝑦 ⊆ 𝑧 → 𝑦 ∈ 𝑥)
6	5	bm1.3ii 4817	. . . . 5 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ⊆ 𝑧)
7		abeq2 2761	. . . . . 6 ⊢ (𝑥 = {𝑦 ∣ 𝑦 ⊆ 𝑧} ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ⊆ 𝑧))
8	7	exbii 1814	. . . . 5 ⊢ (∃𝑥 𝑥 = {𝑦 ∣ 𝑦 ⊆ 𝑧} ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ⊆ 𝑧))
9	6, 8	mpbir 221	. . . 4 ⊢ ∃𝑥 𝑥 = {𝑦 ∣ 𝑦 ⊆ 𝑧}
10	9	issetri 3241	. . 3 ⊢ {𝑦 ∣ 𝑦 ⊆ 𝑧} ∈ V
11	4, 10	eqeltri 2726	. 2 ⊢ 𝒫 𝑧 ∈ V
12	1, 3, 11	vtocl 3290	1 ⊢ 𝒫 𝐴 ∈ V

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