Theorem vpwex 5337

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 5338 from vpwex 5337. (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 4567	. 2 ⊢ 𝒫 𝑥 = {𝑤 ∣ 𝑤 ⊆ 𝑥}
2		axpow2 5327	. . . . 5 ⊢ ∃𝑦∀𝑧(𝑧 ⊆ 𝑥 → 𝑧 ∈ 𝑦)
3	2	bm1.3ii 5264	. . . 4 ⊢ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 ⊆ 𝑥)
4		sseq1 3972	. . . . . 6 ⊢ (𝑤 = 𝑧 → (𝑤 ⊆ 𝑥 ↔ 𝑧 ⊆ 𝑥))
5	4	eqabbw 2808	. . . . 5 ⊢ (𝑦 = {𝑤 ∣ 𝑤 ⊆ 𝑥} ↔ ∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 ⊆ 𝑥))
6	5	exbii 1850	. . . 4 ⊢ (∃𝑦 𝑦 = {𝑤 ∣ 𝑤 ⊆ 𝑥} ↔ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 ⊆ 𝑥))
7	3, 6	mpbir 230	. . 3 ⊢ ∃𝑦 𝑦 = {𝑤 ∣ 𝑤 ⊆ 𝑥}
8	7	issetri 3462	. 2 ⊢ {𝑤 ∣ 𝑤 ⊆ 𝑥} ∈ V
9	1, 8	eqeltri 2828	1 ⊢ 𝒫 𝑥 ∈ V

Syntax hints:   ↔ wb 205  ∀wal 1539   = wceq 1541  ∃wex 1781   ∈ wcel 2106  {cab 2708  Vcvv 3446   ⊆ wss 3913  𝒫 cpw 4565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5261  ax-pow 5325

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930  df-pw 4567

This theorem is referenced by:  pwexg  5338  pwnex  7698  inf3lem7  9579  dfac8  10080  dfac13  10087  ackbij1lem8  10172  dominf  10390  numthcor  10439  dominfac  10518  intwun  10680  wunex2  10683  eltsk2g  10696  inttsk  10719  tskcard  10726  intgru  10759  gruina  10763  axgroth6  10773  ismre  17484  fnmre  17485  mreacs  17552  isacs5lem  18448  pmtrfval  19246  istopon  22298  dmtopon  22309  tgdom  22365  isfbas  23217  bj-snglex  35517  exrecfnpw  35925  pwinfi  41958  ntrrn  42516  ntrf  42517  dssmapntrcls  42522  vsetrec  47268  pgindnf  47281