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	⊢ ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		ax-pow	⊢ ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑣 ( 𝑣 ∈ 𝑧 → 𝑣 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 )
2		elequ1	⊢ ( 𝑣 = 𝑤 → ( 𝑣 ∈ 𝑧 ↔ 𝑤 ∈ 𝑧 ) )
3		elequ1	⊢ ( 𝑣 = 𝑤 → ( 𝑣 ∈ 𝑥 ↔ 𝑤 ∈ 𝑥 ) )
4	2 3	imbi12d	⊢ ( 𝑣 = 𝑤 → ( ( 𝑣 ∈ 𝑧 → 𝑣 ∈ 𝑥 ) ↔ ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) ) )
5	4	cbvalvw	⊢ ( ∀ 𝑣 ( 𝑣 ∈ 𝑧 → 𝑣 ∈ 𝑥 ) ↔ ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) )
6	5	imbi1i	⊢ ( ( ∀ 𝑣 ( 𝑣 ∈ 𝑧 → 𝑣 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ↔ ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) )
7	6	albii	⊢ ( ∀ 𝑧 ( ∀ 𝑣 ( 𝑣 ∈ 𝑧 → 𝑣 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ↔ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) )
8	7	exbii	⊢ ( ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑣 ( 𝑣 ∈ 𝑧 → 𝑣 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ↔ ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) )
9	1 8	mpbi	⊢ ∃ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 )