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

Metamath Proof Explorer

Theorem 2reurmo

Description: Double restricted quantification with restricted existential uniqueness and restricted "at most one", analogous to 2eumo . (Contributed by Alexander van der Vekens, 24-Jun-2017)

		Ref	Expression
	Assertion	2reurmo	$⊢ \exists! x \in A \exists^{} y \in B φ \to \exists^{} x \in A \exists! y \in B φ$

Proof

Step	Hyp	Ref	Expression
1		reuimrmo	$⊢ \forall x \in A (\exists! y \in B φ \to \exists^{} y \in B φ) \to (\exists! x \in A \exists^{} y \in B φ \to \exists^{*} x \in A \exists! y \in B φ)$
2		reurmo	$⊢ \exists! y \in B φ \to \exists^{*} y \in B φ$
3	2	a1i	$⊢ x \in A \to (\exists! y \in B φ \to \exists^{*} y \in B φ)$
4	1 3	mprg	$⊢ \exists! x \in A \exists^{} y \in B φ \to \exists^{} x \in A \exists! y \in B φ$