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 df-ss ⊢ 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