Theorem vpwex 5334

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 5335 from vpwex 5334. (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 4557	. 2 ⊢ 𝒫 𝑥 = {𝑤 ∣ 𝑤 ⊆ 𝑥}
2		axpow2 5324	. . . . 5 ⊢ ∃𝑦∀𝑧(𝑧 ⊆ 𝑥 → 𝑧 ∈ 𝑦)
3	2	sepexi 5251	. . . 4 ⊢ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 ⊆ 𝑥)
4		sseq1 3961	. . . . . 6 ⊢ (𝑤 = 𝑧 → (𝑤 ⊆ 𝑥 ↔ 𝑧 ⊆ 𝑥))
5	4	eqabbw 2835	. . . . 5 ⊢ (𝑦 = {𝑤 ∣ 𝑤 ⊆ 𝑥} ↔ ∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 ⊆ 𝑥))
6	5	exbii 1868	. . . 4 ⊢ (∃𝑦 𝑦 = {𝑤 ∣ 𝑤 ⊆ 𝑥} ↔ ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ 𝑧 ⊆ 𝑥))
7	3, 6	mpbir 233	. . 3 ⊢ ∃𝑦 𝑦 = {𝑤 ∣ 𝑤 ⊆ 𝑥}
8	7	issetri 3473	. 2 ⊢ {𝑤 ∣ 𝑤 ⊆ 𝑥} ∈ V
9	1, 8	eqeltri 2858	1 ⊢ 𝒫 𝑥 ∈ V

Syntax hints:   ↔ wb 208  ∀wal 1558   = wceq 1560  ∃wex 1799   ∈ wcel 2142  {cab 2740  Vcvv 3454   ⊆ wss 3904  𝒫 cpw 4555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246  ax-pow 5322

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-ss 3921  df-pw 4557

This theorem is referenced by:  pwexg  5335  pwnex  7742  inf3lem7  9589  dfac8  10092  dfac13  10099  ackbij1lem8  10182  dominf  10402  numthcor  10451  dominfac  10531  intwun  10693  wunex2  10696  eltsk2g  10709  inttsk  10732  tskcard  10739  intgru  10772  gruina  10776  axgroth6  10786  ismre  17618  fnmre  17619  mreacs  17690  isacs5lem  18577  pmtrfval  19490  istopon  22972  dmtopon  22983  tgdom  23038  isfbas  23889  bj-snglex  37458  exrecfnpw  37875  pwinfi  44140  ntrrn  44698  ntrf  44699  dssmapntrcls  44704  vsetrec  50324  pgindnf  50337