Theorem vpwex 5339

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 5340 from vpwex 5339. (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 4559	. 2 ⊢ 𝒫 𝑥 = {𝑤 ∣ 𝑤 ⊆ 𝑥}
2		axpow2 5329	. . . . 5 ⊢ ∃𝑦∀𝑧(𝑧 ⊆ 𝑥 → 𝑧 ∈ 𝑦)
3	2	sepexi 5256	. . . 4 ⊢ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 ⊆ 𝑥)
4		sseq1 3956	. . . . . 6 ⊢ (𝑤 = 𝑧 → (𝑤 ⊆ 𝑥 ↔ 𝑧 ⊆ 𝑥))
5	4	eqabbw 2834	. . . . 5 ⊢ (𝑦 = {𝑤 ∣ 𝑤 ⊆ 𝑥} ↔ ∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 ⊆ 𝑥))
6	5	exbii 1881	. . . 4 ⊢ (∃𝑦 𝑦 = {𝑤 ∣ 𝑤 ⊆ 𝑥} ↔ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 ⊆ 𝑥))
7	3, 6	mpbir 234	. . 3 ⊢ ∃𝑦 𝑦 = {𝑤 ∣ 𝑤 ⊆ 𝑥}
8	7	issetri 3470	. 2 ⊢ {𝑤 ∣ 𝑤 ⊆ 𝑥} ∈ V
9	1, 8	eqeltri 2857	1 ⊢ 𝒫 𝑥 ∈ V

This proof depends on syntax axioms:   ↔ wb 209  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2145  {cab 2739  Vcvv 3451   ⊆ wss 3899  𝒫 cpw 4557

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pow 5327

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-ss 3916  df-pw 4559

This theorem is used by:  pwexg  5340  pwnex  7773  inf3lem7  9635  dfac8  10214  dfac13  10221  ackbij1lem8  10304  dominf  10523  numthcor  10572  dominfac  10658  intwun  10820  wunex2  10823  eltsk2g  10836  inttsk  10859  tskcard  10866  intgru  10899  gruina  10903  axgroth6  10913  ismre  17760  fnmre  17761  mreacs  17832  isacs5lem  18719  pmtrfval  19664  istopon  23230  dmtopon  23241  tgdom  23296  isfbas  24148  bj-snglex  37886  exrecfnpw  38304  pwinfi  44564  ntrrn  45121  ntrf  45122  dssmapntrcls  45127  vsetrec  50795  pgindnf  50808