Metamath Proof Explorer

Theorem rexss

Description: Restricted existential quantification on a subset in terms of superset. (Contributed by Stefan O'Rear, 3-Apr-2015) Avoid axioms. (Revised by SN, 14-Oct-2025)

		Ref	Expression
	Assertion	rexss	$⊢ A \subseteq B \to (\exists x \in A φ \leftrightarrow \exists x \in B (x \in A \land φ))$

Proof

Step	Hyp	Ref	Expression
1		df-ss	$⊢ A \subseteq B \leftrightarrow \forall x (x \in A \to x \in B)$
2		pm3.41	$⊢ (x \in A \to x \in B) \to ((x \in A \land φ) \to x \in B)$
3	2	pm4.71rd	$⊢ (x \in A \to x \in B) \to ((x \in A \land φ) \leftrightarrow (x \in B \land (x \in A \land φ)))$
4	3	alexbii	$⊢ \forall x (x \in A \to x \in B) \to (\exists x (x \in A \land φ) \leftrightarrow \exists x (x \in B \land (x \in A \land φ)))$
5	1 4	sylbi	$⊢ A \subseteq B \to (\exists x (x \in A \land φ) \leftrightarrow \exists x (x \in B \land (x \in A \land φ)))$
6		df-rex	$⊢ \exists x \in A φ \leftrightarrow \exists x (x \in A \land φ)$
7		df-rex	$⊢ \exists x \in B (x \in A \land φ) \leftrightarrow \exists x (x \in B \land (x \in A \land φ))$
8	5 6 7	3bitr4g	$⊢ A \subseteq B \to (\exists x \in A φ \leftrightarrow \exists x \in B (x \in A \land φ))$