Theorem zfcndpow 4948

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

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 2767	. . . . 5 |- -. A.y y = z
2		exnal 1036	. . . . 5 |- (E.y -. y = z <-> -. A.y y = z)
3	1, 2	mpbir 190	. . . 4 |- E.y -. y = z
4		hbe1 1014	. . . . 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 4933	. . . . 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 1062	. . . 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 1282	. . . . . . . 8 |- (E.x y e. z <-> y e. z)
9		ax-17 969	. . . . . . . . 9 |- (y e. x -> A.z y e. x)
10	9	19.3 1029	. . . . . . . 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 997	. . . . . 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 997	. . . 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 1049	. . 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 1134	. . . . . . 7 |- (w = y -> (w e. z <-> y e. z))
18		elequ1 1134	. . . . . . 7 |- (w = y -> (w e. x <-> y e. x))
19	17, 18	imbi12d 625	. . . . . 6 |- (w = y -> ((w e. z -> w e. x) <-> (y e. z -> y e. x)))
20	19	cbvalv 1312	. . . . 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 997	. . 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 1049	. 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 952   = wceq 954   e. wcel 956  E.wex 978

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-11 965  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-15 1358  ax-ext 1457  ax-sep 2698  ax-nul 2705  ax-pow 2737  ax-reg 4573

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-ral 1646  df-rex 1647  df-v 1808  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408  df-pr 2409

Copyright terms: Public domain