2reu5

Description: Double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification, analogous to 2eu5 and reu3 . (Contributed by Alexander van der Vekens, 17-Jun-2017)

		Ref	Expression
	Assertion	2reu5	$⊢ (\exists! x \in A \exists! y \in B φ \land \forall x \in A \exists^{*} y \in B φ) \leftrightarrow (\exists x \in A \exists y \in B φ \land \exists z \in A \exists w \in B \forall x \in A \forall y \in B (φ \to (x = z \land y = w)))$

Proof

Step	Hyp	Ref	Expression
1		r19.29r	$⊢ (\exists x \in A \exists y \in B φ \land \forall x \in A \forall y \in B (φ \to (x = z \land y = w))) \to \exists x \in A (\exists y \in B φ \land \forall y \in B (φ \to (x = z \land y = w)))$
2		r19.29r	$⊢ (\exists y \in B φ \land \forall y \in B (φ \to (x = z \land y = w))) \to \exists y \in B (φ \land (φ \to (x = z \land y = w)))$
3	2	reximi	$⊢ \exists x \in A (\exists y \in B φ \land \forall y \in B (φ \to (x = z \land y = w))) \to \exists x \in A \exists y \in B (φ \land (φ \to (x = z \land y = w)))$
4		pm3.35	$⊢ (φ \land (φ \to (x = z \land y = w))) \to (x = z \land y = w)$
5	4	reximi	$⊢ \exists y \in B (φ \land (φ \to (x = z \land y = w))) \to \exists y \in B (x = z \land y = w)$
6	5	reximi	$⊢ \exists x \in A \exists y \in B (φ \land (φ \to (x = z \land y = w))) \to \exists x \in A \exists y \in B (x = z \land y = w)$
7		eleq1w	$⊢ x = z \to (x \in A \leftrightarrow z \in A)$
8		eleq1w	$⊢ y = w \to (y \in B \leftrightarrow w \in B)$
9	7 8	bi2anan9	$⊢ (x = z \land y = w) \to ((x \in A \land y \in B) \leftrightarrow (z \in A \land w \in B))$
10	9	biimpac	$⊢ ((x \in A \land y \in B) \land (x = z \land y = w)) \to (z \in A \land w \in B)$
11	10	ancomd	$⊢ ((x \in A \land y \in B) \land (x = z \land y = w)) \to (w \in B \land z \in A)$
12	11	ex	$⊢ (x \in A \land y \in B) \to ((x = z \land y = w) \to (w \in B \land z \in A))$
13	12	rexlimivv	$⊢ \exists x \in A \exists y \in B (x = z \land y = w) \to (w \in B \land z \in A)$
14	1 3 6 13	4syl	$⊢ (\exists x \in A \exists y \in B φ \land \forall x \in A \forall y \in B (φ \to (x = z \land y = w))) \to (w \in B \land z \in A)$
15	14	ex	$⊢ \exists x \in A \exists y \in B φ \to (\forall x \in A \forall y \in B (φ \to (x = z \land y = w)) \to (w \in B \land z \in A))$
16	15	pm4.71rd	$⊢ \exists x \in A \exists y \in B φ \to (\forall x \in A \forall y \in B (φ \to (x = z \land y = w)) \leftrightarrow ((w \in B \land z \in A) \land \forall x \in A \forall y \in B (φ \to (x = z \land y = w))))$
17		anass	$⊢ ((w \in B \land z \in A) \land \forall x \in A \forall y \in B (φ \to (x = z \land y = w))) \leftrightarrow (w \in B \land (z \in A \land \forall x \in A \forall y \in B (φ \to (x = z \land y = w))))$
18	16 17	bitrdi	$⊢ \exists x \in A \exists y \in B φ \to (\forall x \in A \forall y \in B (φ \to (x = z \land y = w)) \leftrightarrow (w \in B \land (z \in A \land \forall x \in A \forall y \in B (φ \to (x = z \land y = w)))))$
19	18	2exbidv	$⊢ \exists x \in A \exists y \in B φ \to (\exists z \exists w \forall x \in A \forall y \in B (φ \to (x = z \land y = w)) \leftrightarrow \exists z \exists w (w \in B \land (z \in A \land \forall x \in A \forall y \in B (φ \to (x = z \land y = w)))))$
20	19	pm5.32i	$⊢ (\exists x \in A \exists y \in B φ \land \exists z \exists w \forall x \in A \forall y \in B (φ \to (x = z \land y = w))) \leftrightarrow (\exists x \in A \exists y \in B φ \land \exists z \exists w (w \in B \land (z \in A \land \forall x \in A \forall y \in B (φ \to (x = z \land y = w)))))$
21		2reu5lem3	$⊢ (\exists! x \in A \exists! y \in B φ \land \forall x \in A \exists^{*} y \in B φ) \leftrightarrow (\exists x \in A \exists y \in B φ \land \exists z \exists w \forall x \in A \forall y \in B (φ \to (x = z \land y = w)))$
22		df-rex	$⊢ \exists z \in A \exists w \in B \forall x \in A \forall y \in B (φ \to (x = z \land y = w)) \leftrightarrow \exists z (z \in A \land \exists w \in B \forall x \in A \forall y \in B (φ \to (x = z \land y = w)))$
23		r19.42v	$⊢ \exists w \in B (z \in A \land \forall x \in A \forall y \in B (φ \to (x = z \land y = w))) \leftrightarrow (z \in A \land \exists w \in B \forall x \in A \forall y \in B (φ \to (x = z \land y = w)))$
24		df-rex	$⊢ \exists w \in B (z \in A \land \forall x \in A \forall y \in B (φ \to (x = z \land y = w))) \leftrightarrow \exists w (w \in B \land (z \in A \land \forall x \in A \forall y \in B (φ \to (x = z \land y = w))))$
25	23 24	bitr3i	$⊢ (z \in A \land \exists w \in B \forall x \in A \forall y \in B (φ \to (x = z \land y = w))) \leftrightarrow \exists w (w \in B \land (z \in A \land \forall x \in A \forall y \in B (φ \to (x = z \land y = w))))$
26	25	exbii	$⊢ \exists z (z \in A \land \exists w \in B \forall x \in A \forall y \in B (φ \to (x = z \land y = w))) \leftrightarrow \exists z \exists w (w \in B \land (z \in A \land \forall x \in A \forall y \in B (φ \to (x = z \land y = w))))$
27	22 26	bitri	$⊢ \exists z \in A \exists w \in B \forall x \in A \forall y \in B (φ \to (x = z \land y = w)) \leftrightarrow \exists z \exists w (w \in B \land (z \in A \land \forall x \in A \forall y \in B (φ \to (x = z \land y = w))))$
28	27	anbi2i	$⊢ (\exists x \in A \exists y \in B φ \land \exists z \in A \exists w \in B \forall x \in A \forall y \in B (φ \to (x = z \land y = w))) \leftrightarrow (\exists x \in A \exists y \in B φ \land \exists z \exists w (w \in B \land (z \in A \land \forall x \in A \forall y \in B (φ \to (x = z \land y = w)))))$
29	20 21 28	3bitr4i	$⊢ (\exists! x \in A \exists! y \in B φ \land \forall x \in A \exists^{*} y \in B φ) \leftrightarrow (\exists x \in A \exists y \in B φ \land \exists z \in A \exists w \in B \forall x \in A \forall y \in B (φ \to (x = z \land y = w)))$

Metamath Proof Explorer

Theorem 2reu5

Proof