Metamath Proof Explorer


Theorem abrexex2

Description: Existence of an existentially restricted class abstraction. ph normally has free-variable parameters x and y . See also abrexex . (Contributed by NM, 12-Sep-2004)

Ref Expression
Hypotheses abrexex2.1
|- A e. _V
abrexex2.2
|- { y | ph } e. _V
Assertion abrexex2
|- { y | E. x e. A ph } e. _V

Proof

Step Hyp Ref Expression
1 abrexex2.1
 |-  A e. _V
2 abrexex2.2
 |-  { y | ph } e. _V
3 2 rgenw
 |-  A. x e. A { y | ph } e. _V
4 abrexex2g
 |-  ( ( A e. _V /\ A. x e. A { y | ph } e. _V ) -> { y | E. x e. A ph } e. _V )
5 1 3 4 mp2an
 |-  { y | E. x e. A ph } e. _V