Theorem abexssex

Description: Existence of a class abstraction with an existentially quantified expression. Both x and y can be free in ph . (Contributed by NM, 29-Jul-2006)

	Ref	Expression
Hypotheses	abrexex2.1	|- A e. _V
	abrexex2.2	|- { y | ph } e. _V
Assertion	abexssex	|- { y | E. x ( x C_ A /\ ph ) } e. _V

Proof

Step	Hyp	Ref	Expression
1		abrexex2.1	|- A e. _V
2		abrexex2.2	|- { y | ph } e. _V
3		df-rex	|- ( E. x e. ~P A ph <-> E. x ( x e. ~P A /\ ph ) )
4		velpw	|- ( x e. ~P A <-> x C_ A )
5	4	anbi1i	|- ( ( x e. ~P A /\ ph ) <-> ( x C_ A /\ ph ) )
6	5	exbii	|- ( E. x ( x e. ~P A /\ ph ) <-> E. x ( x C_ A /\ ph ) )
7	3 6	bitri	|- ( E. x e. ~P A ph <-> E. x ( x C_ A /\ ph ) )
8	7	abbii	|- { y | E. x e. ~P A ph } = { y | E. x ( x C_ A /\ ph ) }
9	1	pwex	|- ~P A e. _V
10	9 2	abrexex2	|- { y | E. x e. ~P A ph } e. _V
11	8 10	eqeltrri	|- { y | E. x ( x C_ A /\ ph ) } e. _V