# Metamath Proof Explorer

## Theorem ssrexf

Description: Restricted existential quantification follows from a subclass relationship. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses ssrexf.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
ssrexf.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
Assertion ssrexf ${⊢}{A}\subseteq {B}\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)$

### Proof

Step Hyp Ref Expression
1 ssrexf.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
2 ssrexf.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
3 1 2 nfss ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{A}\subseteq {B}$
4 ssel ${⊢}{A}\subseteq {B}\to \left({x}\in {A}\to {x}\in {B}\right)$
5 4 anim1d ${⊢}{A}\subseteq {B}\to \left(\left({x}\in {A}\wedge {\phi }\right)\to \left({x}\in {B}\wedge {\phi }\right)\right)$
6 3 5 eximd ${⊢}{A}\subseteq {B}\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge {\phi }\right)\right)$
7 df-rex ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)$
8 df-rex ${⊢}\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\wedge {\phi }\right)$
9 6 7 8 3imtr4g ${⊢}{A}\subseteq {B}\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)$