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 ( 𝐴𝐵 → ( ∃ 𝑥𝐴 𝜑 ↔ ∃ 𝑥𝐵 ( 𝑥𝐴𝜑 ) ) )

Proof

Step Hyp Ref Expression
1 ssel ( 𝐴𝐵 → ( 𝑥𝐴𝑥𝐵 ) )
2 1 pm4.71rd ( 𝐴𝐵 → ( 𝑥𝐴 ↔ ( 𝑥𝐵𝑥𝐴 ) ) )
3 2 anbi1d ( 𝐴𝐵 → ( ( 𝑥𝐴𝜑 ) ↔ ( ( 𝑥𝐵𝑥𝐴 ) ∧ 𝜑 ) ) )
4 anass ( ( ( 𝑥𝐵𝑥𝐴 ) ∧ 𝜑 ) ↔ ( 𝑥𝐵 ∧ ( 𝑥𝐴𝜑 ) ) )
5 3 4 syl6bb ( 𝐴𝐵 → ( ( 𝑥𝐴𝜑 ) ↔ ( 𝑥𝐵 ∧ ( 𝑥𝐴𝜑 ) ) ) )
6 5 rexbidv2 ( 𝐴𝐵 → ( ∃ 𝑥𝐴 𝜑 ↔ ∃ 𝑥𝐵 ( 𝑥𝐴𝜑 ) ) )