This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rsp2e

Description: Restricted specialization. (Contributed by FL, 4-Jun-2012) (Proof shortened by Wolf Lammen, 7-Jan-2020)

		Ref	Expression
	Assertion	rsp2e	$⊢ (x \in A \land y \in B \land φ) \to \exists x \in A \exists y \in B φ$

Step	Hyp	Ref	Expression
1		rspe	$⊢ (y \in B \land φ) \to \exists y \in B φ$
2		rspe	$⊢ (x \in A \land \exists y \in B φ) \to \exists x \in A \exists y \in B φ$
3	1 2	sylan2	$⊢ (x \in A \land (y \in B \land φ)) \to \exists x \in A \exists y \in B φ$
4	3	3impb	$⊢ (x \in A \land y \in B \land φ) \to \exists x \in A \exists y \in B φ$