Theorem vpwex 5316

Description: Power set axiom: the powerclass of a set is a set. Axiom 4 of [TakeutiZaring] p. 17. (Contributed by NM, 30-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) Revised to prove pwexg 5317 from vpwex 5316. (Revised by BJ, 10-Aug-2022.)

Assertion

Ref	Expression
vpwex	⊢ 𝒫 𝑥 ∈ V

Proof of Theorem vpwex

Dummy variables 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-pw 4553	. 2 ⊢ 𝒫 𝑥 = {𝑤 ∣ 𝑤 ⊆ 𝑥}
2		axpow2 5306	. . . . 5 ⊢ ∃𝑦∀𝑧(𝑧 ⊆ 𝑥 → 𝑧 ∈ 𝑦)
3	2	sepexi 5240	. . . 4 ⊢ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 ⊆ 𝑥)
4		sseq1 3961	. . . . . 6 ⊢ (𝑤 = 𝑧 → (𝑤 ⊆ 𝑥 ↔ 𝑧 ⊆ 𝑥))
5	4	eqabbw 2802	. . . . 5 ⊢ (𝑦 = {𝑤 ∣ 𝑤 ⊆ 𝑥} ↔ ∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 ⊆ 𝑥))
6	5	exbii 1848	. . . 4 ⊢ (∃𝑦 𝑦 = {𝑤 ∣ 𝑤 ⊆ 𝑥} ↔ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 ⊆ 𝑥))
7	3, 6	mpbir 231	. . 3 ⊢ ∃𝑦 𝑦 = {𝑤 ∣ 𝑤 ⊆ 𝑥}
8	7	issetri 3455	. 2 ⊢ {𝑤 ∣ 𝑤 ⊆ 𝑥} ∈ V
9	1, 8	eqeltri 2824	1 ⊢ 𝒫 𝑥 ∈ V

Syntax hints:   ↔ wb 206  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2109  {cab 2707  Vcvv 3436   ⊆ wss 3903  𝒫 cpw 4551

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235  ax-pow 5304

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-ss 3920  df-pw 4553

This theorem is referenced by:  pwexg  5317  pwnex  7695  inf3lem7  9530  dfac8  10030  dfac13  10037  ackbij1lem8  10120  dominf  10339  numthcor  10388  dominfac  10467  intwun  10629  wunex2  10632  eltsk2g  10645  inttsk  10668  tskcard  10675  intgru  10708  gruina  10712  axgroth6  10722  ismre  17492  fnmre  17493  mreacs  17564  isacs5lem  18451  pmtrfval  19329  istopon  22797  dmtopon  22808  tgdom  22863  isfbas  23714  bj-snglex  36957  exrecfnpw  37365  pwinfi  43547  ntrrn  44105  ntrf  44106  dssmapntrcls  44111  vsetrec  49698  pgindnf  49711