Theorem vpwex 5079

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 5080 from vpwex 5079. (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 4382	. 2 ⊢ 𝒫 𝑥 = {𝑦 ∣ 𝑦 ⊆ 𝑥}
2		axpow2 5069	. . . . 5 ⊢ ∃𝑧∀𝑦(𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝑧)
3	2	bm1.3ii 5010	. . . 4 ⊢ ∃𝑧∀𝑦(𝑦 ∈ 𝑧 ↔ 𝑦 ⊆ 𝑥)
4		abeq2 2937	. . . . 5 ⊢ (𝑧 = {𝑦 ∣ 𝑦 ⊆ 𝑥} ↔ ∀𝑦(𝑦 ∈ 𝑧 ↔ 𝑦 ⊆ 𝑥))
5	4	exbii 1947	. . . 4 ⊢ (∃𝑧 𝑧 = {𝑦 ∣ 𝑦 ⊆ 𝑥} ↔ ∃𝑧∀𝑦(𝑦 ∈ 𝑧 ↔ 𝑦 ⊆ 𝑥))
6	3, 5	mpbir 223	. . 3 ⊢ ∃𝑧 𝑧 = {𝑦 ∣ 𝑦 ⊆ 𝑥}
7	6	issetri 3427	. 2 ⊢ {𝑦 ∣ 𝑦 ⊆ 𝑥} ∈ V
8	1, 7	eqeltri 2902	1 ⊢ 𝒫 𝑥 ∈ V

Syntax hints:   ↔ wb 198  ∀wal 1654   = wceq 1656  ∃wex 1878   ∈ wcel 2164  {cab 2811  Vcvv 3414   ⊆ wss 3798  𝒫 cpw 4380

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803  ax-sep 5007  ax-pow 5067

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-v 3416  df-in 3805  df-ss 3812  df-pw 4382

This theorem is referenced by:  pwexg  5080  pwnex  7233  inf3lem7  8815  dfac8  9279  dfac13  9286  ackbij1lem8  9371  dominf  9589  numthcor  9638  dominfac  9717  intwun  9879  wunex2  9882  eltsk2g  9895  inttsk  9918  tskcard  9925  intgru  9958  gruina  9962  axgroth6  9972  ismre  16610  fnmre  16611  mreacs  16678  isacs5lem  17529  pmtrfval  18227  istopon  21094  dmtopon  21105  tgdom  21160  isfbas  22010  bj-snglex  33478  pwinfi  38705  ntrrn  39255  ntrf  39256  dssmapntrcls  39261