# Metamath Proof Explorer

## Theorem r19.2z

Description: Theorem 19.2 of Margaris p. 89 with restricted quantifiers (compare 19.2 ). The restricted version is valid only when the domain of quantification is not empty. (Contributed by NM, 15-Nov-2003)

Ref Expression
Assertion r19.2z ${⊢}\left({A}\ne \varnothing \wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$

### Proof

Step Hyp Ref Expression
1 df-ral ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {\phi }\right)$
2 exintr ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {\phi }\right)\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {A}\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)\right)$
3 1 2 sylbi ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {A}\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)\right)$
4 n0 ${⊢}{A}\ne \varnothing ↔\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {A}$
5 df-rex ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)$
6 3 4 5 3imtr4g ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\to \left({A}\ne \varnothing \to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
7 6 impcom ${⊢}\left({A}\ne \varnothing \wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$