Theorem axpow3

Description: A variant of the Axiom of Power Sets ax-pow . For any set x , there exists a set y whose members are exactly the subsets of x i.e. the power set of x . Axiom Pow of BellMachover p. 466. (Contributed by NM, 4-Jun-2006)

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

Proof

Step	Hyp	Ref	Expression
1		axpow2	|- E. y A. z ( z C_ x -> z e. y )
2	1	bm1.3ii	|- E. y A. z ( z e. y <-> z C_ x )
3		bicom	|- ( ( z C_ x <-> z e. y ) <-> ( z e. y <-> z C_ x ) )
4	3	albii	|- ( A. z ( z C_ x <-> z e. y ) <-> A. z ( z e. y <-> z C_ x ) )
5	4	exbii	|- ( E. y A. z ( z C_ x <-> z e. y ) <-> E. y A. z ( z e. y <-> z C_ x ) )
6	2 5	mpbir	|- E. y A. z ( z C_ x <-> z e. y )