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

Metamath Proof Explorer

Theorem 2reu2rex

Description: Double restricted existential uniqueness, analogous to 2eu2ex . (Contributed by Alexander van der Vekens, 25-Jun-2017)

		Ref	Expression
	Assertion	2reu2rex	$⊢ \exists! x \in A \exists! y \in B φ \to \exists x \in A \exists y \in B φ$

Step	Hyp	Ref	Expression
1		reurex	$⊢ \exists! x \in A \exists! y \in B φ \to \exists x \in A \exists! y \in B φ$
2		reurex	$⊢ \exists! y \in B φ \to \exists y \in B φ$
3	2	reximi	$⊢ \exists x \in A \exists! y \in B φ \to \exists x \in A \exists y \in B φ$
4	1 3	syl	$⊢ \exists! x \in A \exists! y \in B φ \to \exists x \in A \exists y \in B φ$