Metamath Proof Explorer


Theorem axpweq

Description: Two equivalent ways to express the Power Set Axiom. Note that ax-pow is not used by the proof. When ax-pow is assumed and A is a set, both sides of the biconditional hold. In ZF, both sides hold if and only if A is a set (see pwexr ). (Contributed by NM, 22-Jun-2009)

Ref Expression
Assertion axpweq 𝒫 A V x y z z y z A y x

Proof

Step Hyp Ref Expression
1 pwidg 𝒫 A V 𝒫 A 𝒫 𝒫 A
2 pweq x = 𝒫 A 𝒫 x = 𝒫 𝒫 A
3 2 eleq2d x = 𝒫 A 𝒫 A 𝒫 x 𝒫 A 𝒫 𝒫 A
4 3 spcegv 𝒫 A V 𝒫 A 𝒫 𝒫 A x 𝒫 A 𝒫 x
5 1 4 mpd 𝒫 A V x 𝒫 A 𝒫 x
6 elex 𝒫 A 𝒫 x 𝒫 A V
7 6 exlimiv x 𝒫 A 𝒫 x 𝒫 A V
8 5 7 impbii 𝒫 A V x 𝒫 A 𝒫 x
9 vex x V
10 9 elpw2 𝒫 A 𝒫 x 𝒫 A x
11 pwss 𝒫 A x y y A y x
12 dfss2 y A z z y z A
13 12 imbi1i y A y x z z y z A y x
14 13 albii y y A y x y z z y z A y x
15 11 14 bitri 𝒫 A x y z z y z A y x
16 10 15 bitri 𝒫 A 𝒫 x y z z y z A y x
17 16 exbii x 𝒫 A 𝒫 x x y z z y z A y x
18 8 17 bitri 𝒫 A V x y z z y z A y x