Theorem axpow2

Description: A variant of the Axiom of Power Sets ax-pow using subset notation. Problem in BellMachover p. 466. (Contributed by NM, 4-Jun-2006)

	Ref	Expression
Assertion	axpow2	|- E. y A. z ( z C_ x -> z e. y )

Proof

Step	Hyp	Ref	Expression
1		ax-pow	|- E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y )
2		df-ss	|- ( z C_ x <-> A. w ( w e. z -> w e. x ) )
3	2	imbi1i	|- ( ( z C_ x -> z e. y ) <-> ( A. w ( w e. z -> w e. x ) -> z e. y ) )
4	3	albii	|- ( A. z ( z C_ x -> z e. y ) <-> A. z ( A. w ( w e. z -> w e. x ) -> z e. y ) )
5	4	exbii	|- ( E. y A. z ( z C_ x -> z e. y ) <-> E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y ) )
6	1 5	mpbir	|- E. y A. z ( z C_ x -> z e. y )