Metamath Proof Explorer

Theorem zfpow

Description: Axiom of Power Sets expressed with the fewest number of different variables. (Contributed by NM, 14-Aug-2003)

Ref Expression
Assertion zfpow ⊢ ∃ x ∀ y ∀ x x ∈ y → x ∈ z → y ∈ x

Proof

Step Hyp Ref Expression
1 ax-pow ⊢ ∃ x ∀ y ∀ w w ∈ y → w ∈ z → y ∈ x
2 elequ1 ⊢ w = x → w ∈ y ↔ x ∈ y
3 elequ1 ⊢ w = x → w ∈ z ↔ x ∈ z
4 2 3 imbi12d ⊢ w = x → w ∈ y → w ∈ z ↔ x ∈ y → x ∈ z
5 4 cbvalvw ⊢ ∀ w w ∈ y → w ∈ z ↔ ∀ x x ∈ y → x ∈ z
6 5 imbi1i ⊢ ∀ w w ∈ y → w ∈ z → y ∈ x ↔ ∀ x x ∈ y → x ∈ z → y ∈ x
7 6 albii ⊢ ∀ y ∀ w w ∈ y → w ∈ z → y ∈ x ↔ ∀ y ∀ x x ∈ y → x ∈ z → y ∈ x
8 7 exbii ⊢ ∃ x ∀ y ∀ w w ∈ y → w ∈ z → y ∈ x ↔ ∃ x ∀ y ∀ x x ∈ y → x ∈ z → y ∈ x
9 1 8 mpbi ⊢ ∃ x ∀ y ∀ x x ∈ y → x ∈ z → y ∈ x