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

Metamath Proof Explorer

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