Theorem pwex 2823

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

Hypothesis

Ref	Expression
zfpowcl.1	|- A e. V

Assertion

Ref	Expression
pwex	|- P~A e. V

Proof of Theorem pwex

Step	Hyp	Ref	Expression
1		zfpowcl.1	. 2 |- A e. V
2		pweq 2460	. . 3 |- (z = A -> P~z = P~A)
3	2	eleq1d 1583	. 2 |- (z = A -> (P~z e. V <-> P~A e. V))
4		zfpow 2819	. . . . . 6 |- E.xA.y(A.x(x e. y -> x e. z) -> y e. x)
5		dfss2 2110	. . . . . . . . 9 |- (y (_ z <-> A.x(x e. y -> x e. z))
6	5	imbi1i 184	. . . . . . . 8 |- ((y (_ z -> y e. x) <-> (A.x(x e. y -> x e. z) -> y e. x))
7	6	albii 1035	. . . . . . 7 |- (A.y(y (_ z -> y e. x) <-> A.y(A.x(x e. y -> x e. z) -> y e. x))
8	7	exbii 1087	. . . . . 6 |- (E.xA.y(y (_ z -> y e. x) <-> E.xA.y(A.x(x e. y -> x e. z) -> y e. x))
9	4, 8	mpbir 188	. . . . 5 |- E.xA.y(y (_ z -> y e. x)
10	9	bm1.3ii 2780	. . . 4 |- E.xA.y(y e. x <-> y (_ z)
11		df-pw 2459	. . . . . . 7 |- P~z = {y | y (_ z}
12	11	eqeq2i 1528	. . . . . 6 |- (x = P~z <-> x = {y | y (_ z})
13		abeq2 1611	. . . . . 6 |- (x = {y | y (_ z} <-> A.y(y e. x <-> y (_ z))
14	12, 13	bitri 171	. . . . 5 |- (x = P~z <-> A.y(y e. x <-> y (_ z))
15	14	exbii 1087	. . . 4 |- (E.x x = P~z <-> E.xA.y(y e. x <-> y (_ z))
16	10, 15	mpbir 188	. . 3 |- E.x x = P~z
17	16	issetri 1862	. 2 |- P~z e. V
18	1, 3, 17	vtocl 1888	1 |- P~A e. V

Syntax hints:   -> wi 3   <-> wb 144  A.wal 990   = wceq 992   e. wcel 994  E.wex 1016  {cab 1505  Vcvv 1857   (_ wss 2099  P~cpw 2458

This theorem is referenced by:  pwexg 2824  snex 2826  pp0ex 2829  ord3ex 2830  abexssex 3986  pw2en 4587  canth2 4629  ssenen 4651  pwfilem 4713  pwfi 4714  inf3lem7 4764  r1suc 4798  rankpw 4830  r1pw 4832  rankss 4834  rankuni 4844  rankc2 4852  rankxpu 4857  rankxplim 4858  aceq3lem 4878  numthlem 4929  numthcor 4932  alephsucpw 5020  dominf 5054  npex 5245  pnfxr 5647  mnfxr 5648  infxpidmlem9 7772  infmap2lem2 7792  gch-kn 7799  distop 7861  issubg 8358  sspval 8636  shex 9353  hsupval2 9576  issubcat 11299  alexsublem2 11497  neibastop2lem1 11580  neibastop2lem4 11583  filssufil 11656  heiborlem23 12033

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-sep 2777  ax-pow 2818

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-v 1858  df-in 2103  df-ss 2105  df-pw 2459

Copyright terms: Public domain