2reu5lem3

Description: Lemma for 2reu5 . This lemma is interesting in its own right, showing that existential restriction in the last conjunct (the "at most one" part) is optional; compare rmo2 . (Contributed by Alexander van der Vekens, 17-Jun-2017)

		Ref	Expression
	Assertion	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)))$

Proof

Step	Hyp	Ref	Expression
1		2reu5lem1	$⊢ \exists! x \in A \exists! y \in B φ \leftrightarrow \exists! x \exists! y (x \in A \land y \in B \land φ)$
2		2reu5lem2	$⊢ \forall x \in A \exists^{} y \in B φ \leftrightarrow \forall x \exists^{} y (x \in A \land y \in B \land φ)$
3	1 2	anbi12i	$⊢ (\exists! x \in A \exists! y \in B φ \land \forall x \in A \exists^{} y \in B φ) \leftrightarrow (\exists! x \exists! y (x \in A \land y \in B \land φ) \land \forall x \exists^{} y (x \in A \land y \in B \land φ))$
4		2eu5	$⊢ (\exists! x \exists! y (x \in A \land y \in B \land φ) \land \forall x \exists^{*} y (x \in A \land y \in B \land φ)) \leftrightarrow (\exists x \exists y (x \in A \land y \in B \land φ) \land \exists z \exists w \forall x \forall y ((x \in A \land y \in B \land φ) \to (x = z \land y = w)))$
5		3anass	$⊢ (x \in A \land y \in B \land φ) \leftrightarrow (x \in A \land (y \in B \land φ))$
6	5	exbii	$⊢ \exists y (x \in A \land y \in B \land φ) \leftrightarrow \exists y (x \in A \land (y \in B \land φ))$
7		19.42v	$⊢ \exists y (x \in A \land (y \in B \land φ)) \leftrightarrow (x \in A \land \exists y (y \in B \land φ))$
8		df-rex	$⊢ \exists y \in B φ \leftrightarrow \exists y (y \in B \land φ)$
9	8	bicomi	$⊢ \exists y (y \in B \land φ) \leftrightarrow \exists y \in B φ$
10	9	anbi2i	$⊢ (x \in A \land \exists y (y \in B \land φ)) \leftrightarrow (x \in A \land \exists y \in B φ)$
11	6 7 10	3bitri	$⊢ \exists y (x \in A \land y \in B \land φ) \leftrightarrow (x \in A \land \exists y \in B φ)$
12	11	exbii	$⊢ \exists x \exists y (x \in A \land y \in B \land φ) \leftrightarrow \exists x (x \in A \land \exists y \in B φ)$
13		df-rex	$⊢ \exists x \in A \exists y \in B φ \leftrightarrow \exists x (x \in A \land \exists y \in B φ)$
14	12 13	bitr4i	$⊢ \exists x \exists y (x \in A \land y \in B \land φ) \leftrightarrow \exists x \in A \exists y \in B φ$
15		3anan12	$⊢ (x \in A \land y \in B \land φ) \leftrightarrow (y \in B \land (x \in A \land φ))$
16	15	imbi1i	$⊢ ((x \in A \land y \in B \land φ) \to (x = z \land y = w)) \leftrightarrow ((y \in B \land (x \in A \land φ)) \to (x = z \land y = w))$
17		impexp	$⊢ ((y \in B \land (x \in A \land φ)) \to (x = z \land y = w)) \leftrightarrow (y \in B \to ((x \in A \land φ) \to (x = z \land y = w)))$
18		impexp	$⊢ ((x \in A \land φ) \to (x = z \land y = w)) \leftrightarrow (x \in A \to (φ \to (x = z \land y = w)))$
19	18	imbi2i	$⊢ (y \in B \to ((x \in A \land φ) \to (x = z \land y = w))) \leftrightarrow (y \in B \to (x \in A \to (φ \to (x = z \land y = w))))$
20	16 17 19	3bitri	$⊢ ((x \in A \land y \in B \land φ) \to (x = z \land y = w)) \leftrightarrow (y \in B \to (x \in A \to (φ \to (x = z \land y = w))))$
21	20	albii	$⊢ \forall y ((x \in A \land y \in B \land φ) \to (x = z \land y = w)) \leftrightarrow \forall y (y \in B \to (x \in A \to (φ \to (x = z \land y = w))))$
22		df-ral	$⊢ \forall y \in B (x \in A \to (φ \to (x = z \land y = w))) \leftrightarrow \forall y (y \in B \to (x \in A \to (φ \to (x = z \land y = w))))$
23		r19.21v	$⊢ \forall y \in B (x \in A \to (φ \to (x = z \land y = w))) \leftrightarrow (x \in A \to \forall y \in B (φ \to (x = z \land y = w)))$
24	21 22 23	3bitr2i	$⊢ \forall y ((x \in A \land y \in B \land φ) \to (x = z \land y = w)) \leftrightarrow (x \in A \to \forall y \in B (φ \to (x = z \land y = w)))$
25	24	albii	$⊢ \forall x \forall y ((x \in A \land y \in B \land φ) \to (x = z \land y = w)) \leftrightarrow \forall x (x \in A \to \forall y \in B (φ \to (x = z \land y = w)))$
26		df-ral	$⊢ \forall x \in A \forall y \in B (φ \to (x = z \land y = w)) \leftrightarrow \forall x (x \in A \to \forall y \in B (φ \to (x = z \land y = w)))$
27	25 26	bitr4i	$⊢ \forall x \forall y ((x \in A \land y \in B \land φ) \to (x = z \land y = w)) \leftrightarrow \forall x \in A \forall y \in B (φ \to (x = z \land y = w))$
28	27	exbii	$⊢ \exists w \forall x \forall y ((x \in A \land y \in B \land φ) \to (x = z \land y = w)) \leftrightarrow \exists w \forall x \in A \forall y \in B (φ \to (x = z \land y = w))$
29	28	exbii	$⊢ \exists z \exists w \forall x \forall y ((x \in A \land y \in B \land φ) \to (x = z \land y = w)) \leftrightarrow \exists z \exists w \forall x \in A \forall y \in B (φ \to (x = z \land y = w))$
30	14 29	anbi12i	$⊢ (\exists x \exists y (x \in A \land y \in B \land φ) \land \exists z \exists w \forall x \forall y ((x \in A \land y \in B \land φ) \to (x = z \land y = w))) \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)))$
31	3 4 30	3bitri	$⊢ (\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)))$

Metamath Proof Explorer

Theorem 2reu5lem3

Proof