Theorem pwex 2713

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 2374	. . 3 |- (z = A -> P~z = P~A)
3	2	eleq1d 1516	. 2 |- (z = A -> (P~z e. V <-> P~A e. V))
4		axpow 2711	. . . . . 6 |- E.xA.y(A.x(x e. y -> x e. z) -> y e. x)
5		dfss2 2029	. . . . . . . . 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 975	. . . . . . 7 |- (A.y(y (_ z -> y e. x) <-> A.y(A.x(x e. y -> x e. z) -> y e. x))
8	7	exbii 1027	. . . . . 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 2674	. . . 4 |- E.xA.y(y e. x <-> y (_ z)
11		df-pw 2373	. . . . . . 7 |- P~z = {y | y (_ z}
12	11	eqeq2i 1461	. . . . . 6 |- (x = P~z <-> x = {y | y (_ z})
13		abeq2 1544	. . . . . 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 1027	. . . 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 1791	. 2 |- P~z e. V
18	1, 3, 17	vtocl 1817	1 |- P~A e. V

Syntax hints:   -> wi 3   <-> wb 146  A.wal 950  E.wex 956   = wceq 1099   e. wcel 1105  {cab 1440  Vcvv 1786   (_ wss 2018  P~cpw 2372

This theorem is referenced by:  pwexg 2714  snex 2718  pp0ex 2739  abexssex 3811  pw2en 4380  canth2 4418  ssenen 4436  pwfilem 4496  pwfi 4497  inf3lem7 4543  r1suc 4576  rankpw 4608  r1pw 4610  rankss 4612  rankuni 4622  rankc2 4630  rankxpu 4635  rankxplim 4636  aceq3lem 4656  numthlem 4707  numthcor 4710  alephsucpw 4793  dominf 4827  npex 5014  pnfxr 5416  mnfxr 5417  mnfnre 5420  pnfnemnf 5460  infxpidmlem9 7454  infmap2lem2 7473  gch-kn 7480  distop 7542  issubg 8001  sspval 8251  shex 9228  hsupval2t 9429

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-13 1107  ax-14 1108  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436  ax-sep 2671  ax-pow 2710

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 957  df-sb 1155  df-clab 1441  df-cleq 1446  df-clel 1449  df-v 1787  df-in 2022  df-ss 2024  df-pw 2373

Copyright terms: Public domain