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 (\exists x \in A φ \leftrightarrow \exists x \in B (x \in A \land φ))$

Step	Hyp	Ref	Expression
1		ssel	$⊢ A \subseteq B \to (x \in A \to x \in B)$
2	1	pm4.71rd	$⊢ A \subseteq B \to (x \in A \leftrightarrow (x \in B \land x \in A))$
3	2	anbi1d	$⊢ A \subseteq B \to ((x \in A \land φ) \leftrightarrow ((x \in B \land x \in A) \land φ))$
4		anass	$⊢ ((x \in B \land x \in A) \land φ) \leftrightarrow (x \in B \land (x \in A \land φ))$
5	3 4	bitrdi	$⊢ A \subseteq B \to ((x \in A \land φ) \leftrightarrow (x \in B \land (x \in A \land φ)))$
6	5	rexbidv2	$⊢ A \subseteq B \to (\exists x \in A φ \leftrightarrow \exists x \in B (x \in A \land φ))$

Metamath Proof Explorer