Theorem zfcndpow 4968

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

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 2772	. . . . 5 |- -. A.y y = z
2		exnal 1038	. . . . 5 |- (E.y -. y = z <-> -. A.y y = z)
3	1, 2	mpbir 190	. . . 4 |- E.y -. y = z
4		hbe1 1016	. . . . 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 4953	. . . . 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 1064	. . . 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 1284	. . . . . . . 8 |- (E.x y e. z <-> y e. z)
9		ax-17 971	. . . . . . . . 9 |- (y e. x -> A.z y e. x)
10	9	19.3 1031	. . . . . . . 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 999	. . . . . 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 999	. . . 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 1051	. . 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 1136	. . . . . . 7 |- (w = y -> (w e. z <-> y e. z))
18		elequ1 1136	. . . . . . 7 |- (w = y -> (w e. x <-> y e. x))
19	17, 18	imbi12d 626	. . . . . 6 |- (w = y -> ((w e. z -> w e. x) <-> (y e. z -> y e. x)))
20	19	cbvalv 1314	. . . . 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 999	. . 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 1051	. 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 954   = wceq 956   e. wcel 958  E.wex 980

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-15 1360  ax-ext 1459  ax-sep 2703  ax-nul 2710  ax-pow 2742  ax-reg 4593

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-ral 1649  df-rex 1650  df-v 1812  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412  df-pr 2413

Copyright terms: Public domain