This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )