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 |
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 |