Metamath Proof Explorer

Theorem r19.37

Description: Restricted quantifier version of one direction of 19.37 . (The other direction does not hold when A is empty.) (Contributed by FL, 13-May-2012) (Revised by Mario Carneiro, 11-Dec-2016)

Ref Expression
Hypothesis r19.37.1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
Assertion r19.37 ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)\to \left({\phi }\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)$

Proof

Step Hyp Ref Expression
1 r19.37.1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
2 r19.35 ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)↔\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
3 ax-1 ${⊢}{\phi }\to \left({x}\in {A}\to {\phi }\right)$
4 1 3 ralrimi ${⊢}{\phi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$
5 4 imim1i ${⊢}\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)\to \left({\phi }\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
6 2 5 sylbi ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)\to \left({\phi }\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)$