Theorem pwex 2740

Description: Power set axiom expressed in class notation. Axiom 4 of [TakeutiZaring] p. 17.

Hypothesis

Ref	Expression
zfpowcl.1	⊢ A ∈ V

Assertion

Ref	Expression
pwex	⊢ ℘A ∈ V

Proof of Theorem pwex

Step	Hyp	Ref	Expression
1		zfpowcl.1	. 2 ⊢ A ∈ V
2		pweq 2399	. . 3 ⊢ (z = A → ℘z = ℘A)
3	2	eleq1d 1537	. 2 ⊢ (z = A → (℘z ∈ V ↔ ℘A ∈ V))
4		axpow 2738	. . . . . 6 ⊢ ∃x∀y(∀x(x ∈ y → x ∈ z) → y ∈ x)
5		dfss2 2054	. . . . . . . . 9 ⊢ (y ⊆ z ↔ ∀x(x ∈ y → x ∈ z))
6	5	imbi1i 186	. . . . . . . 8 ⊢ ((y ⊆ z → y ∈ x) ↔ (∀x(x ∈ y → x ∈ z) → y ∈ x))
7	6	albii 997	. . . . . . 7 ⊢ (∀y(y ⊆ z → y ∈ x) ↔ ∀y(∀x(x ∈ y → x ∈ z) → y ∈ x))
8	7	exbii 1049	. . . . . 6 ⊢ (∃x∀y(y ⊆ z → y ∈ x) ↔ ∃x∀y(∀x(x ∈ y → x ∈ z) → y ∈ x))
9	4, 8	mpbir 190	. . . . 5 ⊢ ∃x∀y(y ⊆ z → y ∈ x)
10	9	bm1.3ii 2701	. . . 4 ⊢ ∃x∀y(y ∈ x ↔ y ⊆ z)
11		df-pw 2398	. . . . . . 7 ⊢ ℘z = {y∣y ⊆ z}
12	11	eqeq2i 1482	. . . . . 6 ⊢ (x = ℘z ↔ x = {y∣y ⊆ z})
13		abeq2 1565	. . . . . 6 ⊢ (x = {y∣y ⊆ z} ↔ ∀y(y ∈ x ↔ y ⊆ z))
14	12, 13	bitr 173	. . . . 5 ⊢ (x = ℘z ↔ ∀y(y ∈ x ↔ y ⊆ z))
15	14	exbii 1049	. . . 4 ⊢ (∃x x = ℘z ↔ ∃x∀y(y ∈ x ↔ y ⊆ z))
16	10, 15	mpbir 190	. . 3 ⊢ ∃x x = ℘z
17	16	issetri 1812	. 2 ⊢ ℘z ∈ V
18	1, 3, 17	vtocl 1838	1 ⊢ ℘A ∈ V

Syntax hints:   → wi 3   ↔ wb 146  ∀wal 952   = wceq 954   ∈ wcel 956  ∃wex 978  {cab 1461  Vcvv 1807   ⊆ wss 2043  ℘cpw 2397

This theorem is referenced by:  pwexg 2741  snex 2745  pp0ex 2766  abexssex 3863  pw2en 4432  canth2 4470  ssenen 4490  pwfilem 4550  pwfi 4551  inf3lem7 4599  r1suc 4632  rankpw 4664  r1pw 4666  rankss 4668  rankuni 4678  rankc2 4686  rankxpu 4691  rankxplim 4692  aceq3lem 4712  numthlem 4763  numthcor 4766  alephsucpw 4850  dominf 4884  npex 5071  pnfxr 5473  mnfxr 5474  pnfnemnf 5517  infxpidmlem9 7511  infmap2lem2 7530  gch-kn 7537  distop 7599  issubg 8068  sspval 8329  shex 9016  hsupval2t 9238

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698  ax-pow 2737

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-in 2047  df-ss 2049  df-pw 2398

Copyright terms: Public domain