# Metamath Proof Explorer

## Theorem rexim

Description: Theorem 19.22 of Margaris p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994) (Proof shortened by Andrew Salmon, 30-May-2011)

Ref Expression
Assertion rexim ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)$

### Proof

Step Hyp Ref Expression
1 con3 ${⊢}\left({\phi }\to {\psi }\right)\to \left(¬{\psi }\to ¬{\phi }\right)$
2 1 ral2imi ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{\psi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{\phi }\right)$
3 2 con3d ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)\to \left(¬\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{\phi }\to ¬\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{\psi }\right)$
4 dfrex2 ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔¬\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{\phi }$
5 dfrex2 ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }↔¬\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{\psi }$
6 3 4 5 3imtr4g ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)$