Description: Inference from Theorem 19.23 of Margaris p. 90 (restricted quantifier version). (Contributed by NM, 18-Dec-2006) Shorten dependent theorems. (Revised by Wolf lammen, 23-Dec-2024)
Ref | Expression | ||
---|---|---|---|
Hypothesis | rexlimiva.1 | |- ( ( x e. A /\ ph ) -> ps ) |
|
Assertion | rexlimiva | |- ( E. x e. A ph -> ps ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexlimiva.1 | |- ( ( x e. A /\ ph ) -> ps ) |
|
2 | df-rex | |- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) ) |
|
3 | 1 | exlimiv | |- ( E. x ( x e. A /\ ph ) -> ps ) |
4 | 2 3 | sylbi | |- ( E. x e. A ph -> ps ) |