Theorem pwex 4769

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 4766	. . . . . 6 ⊢ ∃𝑥∀𝑦(𝑦 ⊆ 𝑧 → 𝑦 ∈ 𝑥)
6	5	bm1.3ii 4707	. . . . 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 4704  ax-pow 4764

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  4770  p0ex  4774  pp0ex  4776  ord3ex  4777  abexssex  7019  fnpm  7730  canth2  7976  dffi3  8198  r1sucg  8493  r1pwALT  8570  rankuni  8587  rankc2  8595  rankxpu  8600  rankmapu  8602  rankxplim  8603  r0weon  8696  aceq3lem  8804  dfac5lem4  8810  dfac2a  8813  dfac2  8814  ackbij2lem2  8923  ackbij2lem3  8924  fin23lem17  9021  domtriomlem  9125  axdc2lem  9131  axdc3lem  9133  axdclem2  9203  alephsucpw  9249  canthp1lem1  9331  gchac  9360  gruina  9497  npex  9665  axcnex  9825  pnfxr  11784  mnfxr  11786  ixxex  12016  prdsval  15887  prdsds  15896  prdshom  15899  ismre  16022  fnmre  16023  fnmrc  16039  mrcfval  16040  mrisval  16062  wunfunc  16331  catcfuccl  16531  catcxpccl  16619  lubfval  16750  glbfval  16763  issubm  17119  issubg  17366  cntzfval  17525  sylow1lem2  17786  lsmfval  17825  pj1fval  17879  issubrg  18552  lssset  18704  lspfval  18743  islbs  18846  lbsext  18933  lbsexg  18934  sraval  18946  aspval  19098  ocvfval  19777  cssval  19793  isobs  19831  islinds  19915  istopon  20488  fncld  20584  leordtval2  20774  cnpfval  20796  iscnp2  20801  kgenf  21102  xkoopn  21150  xkouni  21160  dfac14  21179  xkoccn  21180  prdstopn  21189  xkoco1cn  21218  xkoco2cn  21219  xkococn  21221  xkoinjcn  21248  isfbas  21391  uzrest  21459  acufl  21479  alexsubALTlem2  21610  tsmsval2  21691  ustfn  21763  ustn0  21782  ishtpy  22527  vitali  23133  sspval  26756  shex  27247  hsupval  27371  fpwrelmap  28690  fpwrelmapffs  28691  isrnsigaOLD  29296  dmvlsiga  29313  eulerpartlem1  29550  eulerpartgbij  29555  eulerpartlemmf  29558  coinflippv  29666  ballotlemoex  29668  kur14lem9  30244  mpstval  30480  mclsrcl  30506  mclsval  30508  bj-dmtopon  32036  heibor1lem  32572  heibor  32584  idlval  32776  psubspset  33842  paddfval  33895  pclfvalN  33987  polfvalN  34002  psubclsetN  34034  docafvalN  35223  djafvalN  35235  dicval  35277  dochfval  35451  djhfval  35498  islpolN  35584  mzpclval  36100  eldiophb  36132  rpnnen3  36411  dfac11  36444  rgspnval  36551  clsk1independent  37158  dmvolsal  39034  ovnval  39225  smfresal  39467  issubmgm  41571  lincop  41983