# Metamath Proof Explorer

## Theorem rexss

Description: Restricted existential quantification on a subset in terms of superset. (Contributed by Stefan O'Rear, 3-Apr-2015)

Ref Expression
Assertion rexss ${⊢}{A}\subseteq {B}\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)\right)$

### Proof

Step Hyp Ref Expression
1 ssel ${⊢}{A}\subseteq {B}\to \left({x}\in {A}\to {x}\in {B}\right)$
2 1 pm4.71rd ${⊢}{A}\subseteq {B}\to \left({x}\in {A}↔\left({x}\in {B}\wedge {x}\in {A}\right)\right)$
3 2 anbi1d ${⊢}{A}\subseteq {B}\to \left(\left({x}\in {A}\wedge {\phi }\right)↔\left(\left({x}\in {B}\wedge {x}\in {A}\right)\wedge {\phi }\right)\right)$
4 anass ${⊢}\left(\left({x}\in {B}\wedge {x}\in {A}\right)\wedge {\phi }\right)↔\left({x}\in {B}\wedge \left({x}\in {A}\wedge {\phi }\right)\right)$
5 3 4 syl6bb ${⊢}{A}\subseteq {B}\to \left(\left({x}\in {A}\wedge {\phi }\right)↔\left({x}\in {B}\wedge \left({x}\in {A}\wedge {\phi }\right)\right)\right)$
6 5 rexbidv2 ${⊢}{A}\subseteq {B}\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)\right)$