Metamath Proof Explorer


Theorem rexlimiva

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 )

Proof

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 )