Theorem zfcndpow 4940

Description: Axiom of Power Sets, reproved from conditionless ZFC axioms. The proof uses the "Axiom of Twoness," dtru 2762.

Assertion

Ref	Expression
zfcndpow	|- E.yA.z(A.w(w e. z -> w e. x) -> z e. y)

Distinct variable group:   x,y,z,w

Proof of Theorem zfcndpow

Step	Hyp	Ref	Expression
1		dtru 2762	. . . . 5 |- -. A.y y = z
2		exnal 1034	. . . . 5 |- (E.y -. y = z <-> -. A.y y = z)
3	1, 2	mpbir 190	. . . 4 |- E.y -. y = z
4		hbe1 1012	. . . . 5 |- (E.yA.z(A.y(E.x y e. z -> A.z y e. x) -> z e. y) -> A.yE.yA.z(A.y(E.x y e. z -> A.z y e. x) -> z e. y))
5		axpownd 4925	. . . . 5 |- (-. y = z -> E.yA.z(A.y(E.x y e. z -> A.z y e. x) -> z e. y))
6	4, 5	19.23ai 1060	. . . 4 |- (E.y -. y = z -> E.yA.z(A.y(E.x y e. z -> A.z y e. x) -> z e. y))
7	3, 6	ax-mp 7	. . 3 |- E.yA.z(A.y(E.x y e. z -> A.z y e. x) -> z e. y)
8		19.9v 1279	. . . . . . . 8 |- (E.x y e. z <-> y e. z)
9		ax-17 968	. . . . . . . . 9 |- (y e. x -> A.z y e. x)
10	9	19.3 1027	. . . . . . . 8 |- (A.z y e. x <-> y e. x)
11	8, 10	imbi12i 188	. . . . . . 7 |- ((E.x y e. z -> A.z y e. x) <-> (y e. z -> y e. x))
12	11	albii 996	. . . . . 6 |- (A.y(E.x y e. z -> A.z y e. x) <-> A.y(y e. z -> y e. x))
13	12	imbi1i 186	. . . . 5 |- ((A.y(E.x y e. z -> A.z y e. x) -> z e. y) <-> (A.y(y e. z -> y e. x) -> z e. y))
14	13	albii 996	. . . 4 |- (A.z(A.y(E.x y e. z -> A.z y e. x) -> z e. y) <-> A.z(A.y(y e. z -> y e. x) -> z e. y))
15	14	exbii 1047	. . 3 |- (E.yA.z(A.y(E.x y e. z -> A.z y e. x) -> z e. y) <-> E.yA.z(A.y(y e. z -> y e. x) -> z e. y))
16	7, 15	mpbi 189	. 2 |- E.yA.z(A.y(y e. z -> y e. x) -> z e. y)
17		elequ1 1132	. . . . . . 7 |- (w = y -> (w e. z <-> y e. z))
18		elequ1 1132	. . . . . . 7 |- (w = y -> (w e. x <-> y e. x))
19	17, 18	imbi12d 624	. . . . . 6 |- (w = y -> ((w e. z -> w e. x) <-> (y e. z -> y e. x)))
20	19	cbvalv 1309	. . . . 5 |- (A.w(w e. z -> w e. x) <-> A.y(y e. z -> y e. x))
21	20	imbi1i 186	. . . 4 |- ((A.w(w e. z -> w e. x) -> z e. y) <-> (A.y(y e. z -> y e. x) -> z e. y))
22	21	albii 996	. . 3 |- (A.z(A.w(w e. z -> w e. x) -> z e. y) <-> A.z(A.y(y e. z -> y e. x) -> z e. y))
23	22	exbii 1047	. 2 |- (E.yA.z(A.w(w e. z -> w e. x) -> z e. y) <-> E.yA.z(A.y(y e. z -> y e. x) -> z e. y))
24	16, 23	mpbir 190	1 |- E.yA.z(A.w(w e. z -> w e. x) -> z e. y)

Syntax hints:  -. wn 2   -> wi 3  A.wal 951   = wceq 953   e. wcel 955  E.wex 977

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-11 964  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-15 1353  ax-ext 1452  ax-sep 2693  ax-nul 2700  ax-pow 2732  ax-reg 4565

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-ral 1641  df-rex 1642  df-v 1803  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403

Copyright terms: Public domain