Metamath Proof Explorer

Theorem rexssOLD

Description: Obsolete version of rexss as of 14-Oct-2025. (Contributed by Stefan O'Rear, 3-Apr-2015) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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 φ))$