Metamath Proof Explorer

Theorem axpowg

Description: A generalization of ax-pow that combines it and zfpow into a single theorem scheme. Unlike ax-pow , this scheme lacks a distinct variable condition for y and w . (Contributed by BTernaryTau, 26-May-2026)

Ref Expression
Assertion axpowg ⊢ ∃ y ∀ z ∀ w w ∈ z → w ∈ x → z ∈ y

Proof

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