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	|- E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y )

Proof

Step	Hyp	Ref	Expression
1		ax-pow	|- E. y A. z ( A. v ( v e. z -> v e. x ) -> z e. y )
2		elequ1	|- ( v = w -> ( v e. z <-> w e. z ) )
3		elequ1	|- ( v = w -> ( v e. x <-> w e. x ) )
4	2 3	imbi12d	|- ( v = w -> ( ( v e. z -> v e. x ) <-> ( w e. z -> w e. x ) ) )
5	4	cbvalvw	|- ( A. v ( v e. z -> v e. x ) <-> A. w ( w e. z -> w e. x ) )
6	5	imbi1i	|- ( ( A. v ( v e. z -> v e. x ) -> z e. y ) <-> ( A. w ( w e. z -> w e. x ) -> z e. y ) )
7	6	albii	|- ( A. z ( A. v ( v e. z -> v e. x ) -> z e. y ) <-> A. z ( A. w ( w e. z -> w e. x ) -> z e. y ) )
8	7	exbii	|- ( E. y A. z ( A. v ( v e. z -> v e. x ) -> z e. y ) <-> E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y ) )
9	1 8	mpbi	|- E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y )