Theorem abssexg

Description: Existence of a class of subsets. (Contributed by NM, 15-Jul-2006) (Proof shortened by Andrew Salmon, 25-Jul-2011)

	Ref	Expression
Assertion	abssexg	|- ( A e. V -> { x | ( x C_ A /\ ph ) } e. _V )

Proof

Step	Hyp	Ref	Expression
1		pwexg	|- ( A e. V -> ~P A e. _V )
2		df-pw	|- ~P A = { x | x C_ A }
3	2	eleq1i	|- ( ~P A e. _V <-> { x | x C_ A } e. _V )
4		simpl	|- ( ( x C_ A /\ ph ) -> x C_ A )
5	4	ss2abi	|- { x | ( x C_ A /\ ph ) } C_ { x | x C_ A }
6		ssexg	|- ( ( { x | ( x C_ A /\ ph ) } C_ { x | x C_ A } /\ { x | x C_ A } e. _V ) -> { x | ( x C_ A /\ ph ) } e. _V )
7	5 6	mpan	|- ( { x | x C_ A } e. _V -> { x | ( x C_ A /\ ph ) } e. _V )
8	3 7	sylbi	|- ( ~P A e. _V -> { x | ( x C_ A /\ ph ) } e. _V )
9	1 8	syl	|- ( A e. V -> { x | ( x C_ A /\ ph ) } e. _V )