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 ( ( 𝑥𝐴𝜑 ) → 𝜓 )
Assertion rexlimiva ( ∃ 𝑥𝐴 𝜑𝜓 )

Proof

Step Hyp Ref Expression
1 rexlimiva.1 ( ( 𝑥𝐴𝜑 ) → 𝜓 )
2 df-rex ( ∃ 𝑥𝐴 𝜑 ↔ ∃ 𝑥 ( 𝑥𝐴𝜑 ) )
3 1 exlimiv ( ∃ 𝑥 ( 𝑥𝐴𝜑 ) → 𝜓 )
4 2 3 sylbi ( ∃ 𝑥𝐴 𝜑𝜓 )