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	bitrdi	⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ) )
6	5	rexbidv2	⊢ ( 𝐴 ⊆ 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ∈ 𝐵 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )