Metamath Proof Explorer

Theorem 2reu5a

Description: Double restricted existential uniqueness in terms of restricted existence and restricted "at most one". (Contributed by Alexander van der Vekens, 17-Jun-2017)

		Ref	Expression
	Assertion	2reu5a	$⊢ \exists! x \in A \exists! y \in B φ \leftrightarrow (\exists x \in A (\exists y \in B φ \land \exists^{} y \in B φ) \land \exists^{} x \in A (\exists y \in B φ \land \exists^{*} y \in B φ))$

Proof

Step	Hyp	Ref	Expression
1		reu5	$⊢ \exists! x \in A \exists! y \in B φ \leftrightarrow (\exists x \in A \exists! y \in B φ \land \exists^{*} x \in A \exists! y \in B φ)$
2		reu5	$⊢ \exists! y \in B φ \leftrightarrow (\exists y \in B φ \land \exists^{*} y \in B φ)$
3	2	rexbii	$⊢ \exists x \in A \exists! y \in B φ \leftrightarrow \exists x \in A (\exists y \in B φ \land \exists^{*} y \in B φ)$
4	2	rmobii	$⊢ \exists^{} x \in A \exists! y \in B φ \leftrightarrow \exists^{} x \in A (\exists y \in B φ \land \exists^{*} y \in B φ)$
5	3 4	anbi12i	$⊢ (\exists x \in A \exists! y \in B φ \land \exists^{} x \in A \exists! y \in B φ) \leftrightarrow (\exists x \in A (\exists y \in B φ \land \exists^{} y \in B φ) \land \exists^{} x \in A (\exists y \in B φ \land \exists^{} y \in B φ))$
6	1 5	bitri	$⊢ \exists! x \in A \exists! y \in B φ \leftrightarrow (\exists x \in A (\exists y \in B φ \land \exists^{} y \in B φ) \land \exists^{} x \in A (\exists y \in B φ \land \exists^{*} y \in B φ))$