Theorem pwex 4848

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 4161	. . 3 ⊢ (𝑧 = 𝐴 → 𝒫 𝑧 = 𝒫 𝐴)
3	2	eleq1d 2686	. 2 ⊢ (𝑧 = 𝐴 → (𝒫 𝑧 ∈ V ↔ 𝒫 𝐴 ∈ V))
4		df-pw 4160	. . 3 ⊢ 𝒫 𝑧 = {𝑦 ∣ 𝑦 ⊆ 𝑧}
5		axpow2 4845	. . . . . 6 ⊢ ∃𝑥∀𝑦(𝑦 ⊆ 𝑧 → 𝑦 ∈ 𝑥)
6	5	bm1.3ii 4784	. . . . 5 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ⊆ 𝑧)
7		abeq2 2732	. . . . . 6 ⊢ (𝑥 = {𝑦 ∣ 𝑦 ⊆ 𝑧} ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ⊆ 𝑧))
8	7	exbii 1774	. . . . 5 ⊢ (∃𝑥 𝑥 = {𝑦 ∣ 𝑦 ⊆ 𝑧} ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ⊆ 𝑧))
9	6, 8	mpbir 221	. . . 4 ⊢ ∃𝑥 𝑥 = {𝑦 ∣ 𝑦 ⊆ 𝑧}
10	9	issetri 3210	. . 3 ⊢ {𝑦 ∣ 𝑦 ⊆ 𝑧} ∈ V
11	4, 10	eqeltri 2697	. 2 ⊢ 𝒫 𝑧 ∈ V
12	1, 3, 11	vtocl 3259	1 ⊢ 𝒫 𝐴 ∈ V

Syntax hints:   ↔ wb 196  ∀wal 1481   = wceq 1483  ∃wex 1704   ∈ wcel 1990  {cab 2608  Vcvv 3200   ⊆ wss 3574  𝒫 cpw 4158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-pow 4843

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-v 3202  df-in 3581  df-ss 3588  df-pw 4160

This theorem is referenced by:  vpwex  4849  p0ex  4853  pp0ex  4855  ord3ex  4856  abexssex  7149  fnpm  7865  canth2  8113  dffi3  8337  r1sucg  8632  r1pwALT  8709  rankuni  8726  rankc2  8734  rankxpu  8739  rankmapu  8741  rankxplim  8742  r0weon  8835  aceq3lem  8943  dfac5lem4  8949  dfac2a  8952  dfac2  8953  ackbij2lem2  9062  ackbij2lem3  9063  fin23lem17  9160  domtriomlem  9264  axdc2lem  9270  axdc3lem  9272  axdclem2  9342  alephsucpw  9392  canthp1lem1  9474  gchac  9503  gruina  9640  npex  9808  axcnex  9968  pnfxr  10092  mnfxr  10096  ixxex  12186  prdsval  16115  prdsds  16124  prdshom  16127  ismre  16250  fnmre  16251  fnmrc  16267  mrcfval  16268  mrisval  16290  wunfunc  16559  catcfuccl  16759  catcxpccl  16847  lubfval  16978  glbfval  16991  issubm  17347  issubg  17594  cntzfval  17753  sylow1lem2  18014  lsmfval  18053  pj1fval  18107  issubrg  18780  lssset  18934  lspfval  18973  islbs  19076  lbsext  19163  lbsexg  19164  sraval  19176  aspval  19328  ocvfval  20010  cssval  20026  isobs  20064  islinds  20148  istopon  20717  dmtopon  20727  fncld  20826  leordtval2  21016  cnpfval  21038  iscnp2  21043  kgenf  21344  xkoopn  21392  xkouni  21402  dfac14  21421  xkoccn  21422  prdstopn  21431  xkoco1cn  21460  xkoco2cn  21461  xkococn  21463  xkoinjcn  21490  isfbas  21633  uzrest  21701  acufl  21721  alexsubALTlem2  21852  tsmsval2  21933  ustfn  22005  ustn0  22024  ishtpy  22771  vitali  23382  sspval  27578  shex  28069  hsupval  28193  fpwrelmap  29508  fpwrelmapffs  29509  isrnsigaOLD  30175  dmvlsiga  30192  eulerpartlem1  30429  eulerpartgbij  30434  eulerpartlemmf  30437  coinflippv  30545  ballotlemoex  30547  reprval  30688  kur14lem9  31196  mpstval  31432  mclsrcl  31458  mclsval  31460  heibor1lem  33608  heibor  33620  idlval  33812  psubspset  35030  paddfval  35083  pclfvalN  35175  polfvalN  35190  psubclsetN  35222  docafvalN  36411  djafvalN  36423  dicval  36465  dochfval  36639  djhfval  36686  islpolN  36772  mzpclval  37288  eldiophb  37320  rpnnen3  37599  dfac11  37632  rgspnval  37738  clsk1independent  38344  dmvolsal  40564  ovnval  40755  smfresal  40995  sprbisymrel  41749  uspgrex  41758  uspgrbisymrelALT  41763  issubmgm  41789  lincop  42197  setrec2fun  42439  vsetrec  42446  elpglem3  42456