Theorem pwex 2735

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 2393	. . 3 |- (z = A -> P~z = P~A)
3	2	eleq1d 1532	. 2 |- (z = A -> (P~z e. V <-> P~A e. V))
4		axpow 2733	. . . . . 6 |- E.xA.y(A.x(x e. y -> x e. z) -> y e. x)
5		dfss2 2048	. . . . . . . . 9 |- (y (_ z <-> A.x(x e. y -> x e. z))
6	5	imbi1i 186	. . . . . . . 8 |- ((y (_ z -> y e. x) <-> (A.x(x e. y -> x e. z) -> y e. x))
7	6	albii 996	. . . . . . 7 |- (A.y(y (_ z -> y e. x) <-> A.y(A.x(x e. y -> x e. z) -> y e. x))
8	7	exbii 1047	. . . . . 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 190	. . . . 5 |- E.xA.y(y (_ z -> y e. x)
10	9	bm1.3ii 2696	. . . 4 |- E.xA.y(y e. x <-> y (_ z)
11		df-pw 2392	. . . . . . 7 |- P~z = {y | y (_ z}
12	11	eqeq2i 1477	. . . . . 6 |- (x = P~z <-> x = {y | y (_ z})
13		abeq2 1560	. . . . . 6 |- (x = {y | y (_ z} <-> A.y(y e. x <-> y (_ z))
14	12, 13	bitr 173	. . . . 5 |- (x = P~z <-> A.y(y e. x <-> y (_ z))
15	14	exbii 1047	. . . 4 |- (E.x x = P~z <-> E.xA.y(y e. x <-> y (_ z))
16	10, 15	mpbir 190	. . 3 |- E.x x = P~z
17	16	issetri 1807	. 2 |- P~z e. V
18	1, 3, 17	vtocl 1833	1 |- P~A e. V

Syntax hints:   -> wi 3   <-> wb 146  A.wal 951   = wceq 953   e. wcel 955  E.wex 977  {cab 1456  Vcvv 1802   (_ wss 2037  P~cpw 2391

This theorem is referenced by:  pwexg 2736  snex 2740  pp0ex 2761  abexssex 3857  pw2en 4426  canth2 4464  2pwuninel 4465  ssenen 4484  pwfilem 4544  pwfi 4545  inf3lem7 4591  r1suc 4624  rankpw 4656  r1pw 4658  rankss 4660  rankuni 4670  rankc2 4678  rankxpu 4683  rankxplim 4684  aceq3lem 4704  numthlem 4755  numthcor 4758  alephsucpw 4842  dominf 4876  npex 5063  pnfxr 5465  mnfxr 5466  pnfnemnf 5509  infxpidmlem9 7503  infmap2lem2 7522  gch-kn 7529  distop 7591  issubg 8053  sspval 8316  shex 8998  hsupval2t 9215

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693  ax-pow 2732

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803  df-in 2041  df-ss 2043  df-pw 2392

Copyright terms: Public domain