2reu4lem

		Ref	Expression
	Assertion	2reu4lem	$⊢ (A \neq \emptyset \land B \neq \emptyset) \to ((\exists! x \in A \exists y \in B φ \land \exists! y \in B \exists x \in A φ) \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		reu3	$⊢ \exists! x \in A \exists y \in B φ \leftrightarrow (\exists x \in A \exists y \in B φ \land \exists z \in A \forall x \in A (\exists y \in B φ \to x = z))$
2		reu3	$⊢ \exists! y \in B \exists x \in A φ \leftrightarrow (\exists y \in B \exists x \in A φ \land \exists w \in B \forall y \in B (\exists x \in A φ \to y = w))$
3	1 2	anbi12i	$⊢ (\exists! x \in A \exists y \in B φ \land \exists! y \in B \exists x \in A φ) \leftrightarrow ((\exists x \in A \exists y \in B φ \land \exists z \in A \forall x \in A (\exists y \in B φ \to x = z)) \land (\exists y \in B \exists x \in A φ \land \exists w \in B \forall y \in B (\exists x \in A φ \to y = w)))$
4	3	a1i	$⊢ (A \neq \emptyset \land B \neq \emptyset) \to ((\exists! x \in A \exists y \in B φ \land \exists! y \in B \exists x \in A φ) \leftrightarrow ((\exists x \in A \exists y \in B φ \land \exists z \in A \forall x \in A (\exists y \in B φ \to x = z)) \land (\exists y \in B \exists x \in A φ \land \exists w \in B \forall y \in B (\exists x \in A φ \to y = w))))$
5		an4	$⊢ ((\exists x \in A \exists y \in B φ \land \exists z \in A \forall x \in A (\exists y \in B φ \to x = z)) \land (\exists y \in B \exists x \in A φ \land \exists w \in B \forall y \in B (\exists x \in A φ \to y = w))) \leftrightarrow ((\exists x \in A \exists y \in B φ \land \exists y \in B \exists x \in A φ) \land (\exists z \in A \forall x \in A (\exists y \in B φ \to x = z) \land \exists w \in B \forall y \in B (\exists x \in A φ \to y = w)))$
6	5	a1i	$⊢ (A \neq \emptyset \land B \neq \emptyset) \to (((\exists x \in A \exists y \in B φ \land \exists z \in A \forall x \in A (\exists y \in B φ \to x = z)) \land (\exists y \in B \exists x \in A φ \land \exists w \in B \forall y \in B (\exists x \in A φ \to y = w))) \leftrightarrow ((\exists x \in A \exists y \in B φ \land \exists y \in B \exists x \in A φ) \land (\exists z \in A \forall x \in A (\exists y \in B φ \to x = z) \land \exists w \in B \forall y \in B (\exists x \in A φ \to y = w))))$
7		rexcom	$⊢ \exists y \in B \exists x \in A φ \leftrightarrow \exists x \in A \exists y \in B φ$
8	7	anbi2i	$⊢ (\exists x \in A \exists y \in B φ \land \exists y \in B \exists x \in A φ) \leftrightarrow (\exists x \in A \exists y \in B φ \land \exists x \in A \exists y \in B φ)$
9		anidm	$⊢ (\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 φ$
10	8 9	bitri	$⊢ (\exists x \in A \exists y \in B φ \land \exists y \in B \exists x \in A φ) \leftrightarrow \exists x \in A \exists y \in B φ$
11	10	a1i	$⊢ (A \neq \emptyset \land B \neq \emptyset) \to ((\exists x \in A \exists y \in B φ \land \exists y \in B \exists x \in A φ) \leftrightarrow \exists x \in A \exists y \in B φ)$
12		r19.26	$⊢ \forall x \in A (\forall y \in B (φ \to x = z) \land \forall x \in A \forall y \in B (φ \to y = w)) \leftrightarrow (\forall x \in A \forall y \in B (φ \to x = z) \land \forall x \in A \forall x \in A \forall y \in B (φ \to y = w))$
13		nfra1	$⊢ Ⅎ x \forall x \in A \forall y \in B (φ \to y = w)$
14	13	r19.3rz	$⊢ A \neq \emptyset \to (\forall x \in A \forall y \in B (φ \to y = w) \leftrightarrow \forall x \in A \forall x \in A \forall y \in B (φ \to y = w))$
15	14	bicomd	$⊢ A \neq \emptyset \to (\forall x \in A \forall x \in A \forall y \in B (φ \to y = w) \leftrightarrow \forall x \in A \forall y \in B (φ \to y = w))$
16	15	adantr	$⊢ (A \neq \emptyset \land B \neq \emptyset) \to (\forall x \in A \forall x \in A \forall y \in B (φ \to y = w) \leftrightarrow \forall x \in A \forall y \in B (φ \to y = w))$
17	16	adantr	$⊢ ((A \neq \emptyset \land B \neq \emptyset) \land (z \in A \land w \in B)) \to (\forall x \in A \forall x \in A \forall y \in B (φ \to y = w) \leftrightarrow \forall x \in A \forall y \in B (φ \to y = w))$
18	17	anbi2d	$⊢ ((A \neq \emptyset \land B \neq \emptyset) \land (z \in A \land w \in B)) \to ((\forall x \in A \forall y \in B (φ \to x = z) \land \forall x \in A \forall x \in A \forall y \in B (φ \to y = w)) \leftrightarrow (\forall x \in A \forall y \in B (φ \to x = z) \land \forall x \in A \forall y \in B (φ \to y = w)))$
19		jcab	$⊢ (φ \to (x = z \land y = w)) \leftrightarrow ((φ \to x = z) \land (φ \to y = w))$
20	19	ralbii	$⊢ \forall y \in B (φ \to (x = z \land y = w)) \leftrightarrow \forall y \in B ((φ \to x = z) \land (φ \to y = w))$
21		r19.26	$⊢ \forall y \in B ((φ \to x = z) \land (φ \to y = w)) \leftrightarrow (\forall y \in B (φ \to x = z) \land \forall y \in B (φ \to y = w))$
22	20 21	bitri	$⊢ \forall y \in B (φ \to (x = z \land y = w)) \leftrightarrow (\forall y \in B (φ \to x = z) \land \forall y \in B (φ \to y = w))$
23	22	ralbii	$⊢ \forall x \in A \forall y \in B (φ \to (x = z \land y = w)) \leftrightarrow \forall x \in A (\forall y \in B (φ \to x = z) \land \forall y \in B (φ \to y = w))$
24		r19.26	$⊢ \forall x \in A (\forall y \in B (φ \to x = z) \land \forall y \in B (φ \to y = w)) \leftrightarrow (\forall x \in A \forall y \in B (φ \to x = z) \land \forall x \in A \forall y \in B (φ \to y = w))$
25	23 24	bitri	$⊢ \forall x \in A \forall y \in B (φ \to (x = z \land y = w)) \leftrightarrow (\forall x \in A \forall y \in B (φ \to x = z) \land \forall x \in A \forall y \in B (φ \to y = w))$
26	25	a1i	$⊢ ((A \neq \emptyset \land B \neq \emptyset) \land (z \in A \land w \in B)) \to (\forall x \in A \forall y \in B (φ \to (x = z \land y = w)) \leftrightarrow (\forall x \in A \forall y \in B (φ \to x = z) \land \forall x \in A \forall y \in B (φ \to y = w)))$
27	18 26	bitr4d	$⊢ ((A \neq \emptyset \land B \neq \emptyset) \land (z \in A \land w \in B)) \to ((\forall x \in A \forall y \in B (φ \to x = z) \land \forall x \in A \forall x \in A \forall y \in B (φ \to y = w)) \leftrightarrow \forall x \in A \forall y \in B (φ \to (x = z \land y = w)))$
28	12 27	bitr2id	$⊢ ((A \neq \emptyset \land B \neq \emptyset) \land (z \in A \land w \in B)) \to (\forall x \in A \forall y \in B (φ \to (x = z \land y = w)) \leftrightarrow \forall x \in A (\forall y \in B (φ \to x = z) \land \forall x \in A \forall y \in B (φ \to y = w)))$
29		r19.26	$⊢ \forall y \in B (\forall y \in B (φ \to x = z) \land \forall x \in A (φ \to y = w)) \leftrightarrow (\forall y \in B \forall y \in B (φ \to x = z) \land \forall y \in B \forall x \in A (φ \to y = w))$
30		nfra1	$⊢ Ⅎ y \forall y \in B (φ \to x = z)$
31	30	r19.3rz	$⊢ B \neq \emptyset \to (\forall y \in B (φ \to x = z) \leftrightarrow \forall y \in B \forall y \in B (φ \to x = z))$
32	31	ad2antlr	$⊢ ((A \neq \emptyset \land B \neq \emptyset) \land (z \in A \land w \in B)) \to (\forall y \in B (φ \to x = z) \leftrightarrow \forall y \in B \forall y \in B (φ \to x = z))$
33	32	bicomd	$⊢ ((A \neq \emptyset \land B \neq \emptyset) \land (z \in A \land w \in B)) \to (\forall y \in B \forall y \in B (φ \to x = z) \leftrightarrow \forall y \in B (φ \to x = z))$
34		ralcom	$⊢ \forall y \in B \forall x \in A (φ \to y = w) \leftrightarrow \forall x \in A \forall y \in B (φ \to y = w)$
35	34	a1i	$⊢ ((A \neq \emptyset \land B \neq \emptyset) \land (z \in A \land w \in B)) \to (\forall y \in B \forall x \in A (φ \to y = w) \leftrightarrow \forall x \in A \forall y \in B (φ \to y = w))$
36	33 35	anbi12d	$⊢ ((A \neq \emptyset \land B \neq \emptyset) \land (z \in A \land w \in B)) \to ((\forall y \in B \forall y \in B (φ \to x = z) \land \forall y \in B \forall x \in A (φ \to y = w)) \leftrightarrow (\forall y \in B (φ \to x = z) \land \forall x \in A \forall y \in B (φ \to y = w)))$
37	29 36	syl5bb	$⊢ ((A \neq \emptyset \land B \neq \emptyset) \land (z \in A \land w \in B)) \to (\forall y \in B (\forall y \in B (φ \to x = z) \land \forall x \in A (φ \to y = w)) \leftrightarrow (\forall y \in B (φ \to x = z) \land \forall x \in A \forall y \in B (φ \to y = w)))$
38	37	ralbidv	$⊢ ((A \neq \emptyset \land B \neq \emptyset) \land (z \in A \land w \in B)) \to (\forall x \in A \forall y \in B (\forall y \in B (φ \to x = z) \land \forall x \in A (φ \to y = w)) \leftrightarrow \forall x \in A (\forall y \in B (φ \to x = z) \land \forall x \in A \forall y \in B (φ \to y = w)))$
39	28 38	bitr4d	$⊢ ((A \neq \emptyset \land B \neq \emptyset) \land (z \in A \land w \in B)) \to (\forall x \in A \forall y \in B (φ \to (x = z \land y = w)) \leftrightarrow \forall x \in A \forall y \in B (\forall y \in B (φ \to x = z) \land \forall x \in A (φ \to y = w)))$
40		r19.23v	$⊢ \forall y \in B (φ \to x = z) \leftrightarrow (\exists y \in B φ \to x = z)$
41		r19.23v	$⊢ \forall x \in A (φ \to y = w) \leftrightarrow (\exists x \in A φ \to y = w)$
42	40 41	anbi12i	$⊢ (\forall y \in B (φ \to x = z) \land \forall x \in A (φ \to y = w)) \leftrightarrow ((\exists y \in B φ \to x = z) \land (\exists x \in A φ \to y = w))$
43	42	2ralbii	$⊢ \forall x \in A \forall y \in B (\forall y \in B (φ \to x = z) \land \forall x \in A (φ \to y = w)) \leftrightarrow \forall x \in A \forall y \in B ((\exists y \in B φ \to x = z) \land (\exists x \in A φ \to y = w))$
44	43	a1i	$⊢ ((A \neq \emptyset \land B \neq \emptyset) \land (z \in A \land w \in B)) \to (\forall x \in A \forall y \in B (\forall y \in B (φ \to x = z) \land \forall x \in A (φ \to y = w)) \leftrightarrow \forall x \in A \forall y \in B ((\exists y \in B φ \to x = z) \land (\exists x \in A φ \to y = w)))$
45		neneq	$⊢ A \neq \emptyset \to \neg A = \emptyset$
46		neneq	$⊢ B \neq \emptyset \to \neg B = \emptyset$
47	45 46	anim12i	$⊢ (A \neq \emptyset \land B \neq \emptyset) \to (\neg A = \emptyset \land \neg B = \emptyset)$
48	47	olcd	$⊢ (A \neq \emptyset \land B \neq \emptyset) \to ((A = \emptyset \land B = \emptyset) \lor (\neg A = \emptyset \land \neg B = \emptyset))$
49		dfbi3	$⊢ (A = \emptyset \leftrightarrow B = \emptyset) \leftrightarrow ((A = \emptyset \land B = \emptyset) \lor (\neg A = \emptyset \land \neg B = \emptyset))$
50	48 49	sylibr	$⊢ (A \neq \emptyset \land B \neq \emptyset) \to (A = \emptyset \leftrightarrow B = \emptyset)$
51		nfre1	$⊢ Ⅎ y \exists y \in B φ$
52		nfv	$⊢ Ⅎ y x = z$
53	51 52	nfim	$⊢ Ⅎ y (\exists y \in B φ \to x = z)$
54		nfre1	$⊢ Ⅎ x \exists x \in A φ$
55		nfv	$⊢ Ⅎ x y = w$
56	54 55	nfim	$⊢ Ⅎ x (\exists x \in A φ \to y = w)$
57	53 56	raaan2	$⊢ (A = \emptyset \leftrightarrow B = \emptyset) \to (\forall x \in A \forall y \in B ((\exists y \in B φ \to x = z) \land (\exists x \in A φ \to y = w)) \leftrightarrow (\forall x \in A (\exists y \in B φ \to x = z) \land \forall y \in B (\exists x \in A φ \to y = w)))$
58	50 57	syl	$⊢ (A \neq \emptyset \land B \neq \emptyset) \to (\forall x \in A \forall y \in B ((\exists y \in B φ \to x = z) \land (\exists x \in A φ \to y = w)) \leftrightarrow (\forall x \in A (\exists y \in B φ \to x = z) \land \forall y \in B (\exists x \in A φ \to y = w)))$
59	58	adantr	$⊢ ((A \neq \emptyset \land B \neq \emptyset) \land (z \in A \land w \in B)) \to (\forall x \in A \forall y \in B ((\exists y \in B φ \to x = z) \land (\exists x \in A φ \to y = w)) \leftrightarrow (\forall x \in A (\exists y \in B φ \to x = z) \land \forall y \in B (\exists x \in A φ \to y = w)))$
60	39 44 59	3bitrd	$⊢ ((A \neq \emptyset \land B \neq \emptyset) \land (z \in A \land w \in B)) \to (\forall x \in A \forall y \in B (φ \to (x = z \land y = w)) \leftrightarrow (\forall x \in A (\exists y \in B φ \to x = z) \land \forall y \in B (\exists x \in A φ \to y = w)))$
61	60	2rexbidva	$⊢ (A \neq \emptyset \land B \neq \emptyset) \to (\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 \in A \exists w \in B (\forall x \in A (\exists y \in B φ \to x = z) \land \forall y \in B (\exists x \in A φ \to y = w)))$
62		reeanv	$⊢ \exists z \in A \exists w \in B (\forall x \in A (\exists y \in B φ \to x = z) \land \forall y \in B (\exists x \in A φ \to y = w)) \leftrightarrow (\exists z \in A \forall x \in A (\exists y \in B φ \to x = z) \land \exists w \in B \forall y \in B (\exists x \in A φ \to y = w))$
63	61 62	bitr2di	$⊢ (A \neq \emptyset \land B \neq \emptyset) \to ((\exists z \in A \forall x \in A (\exists y \in B φ \to x = z) \land \exists w \in B \forall y \in B (\exists x \in A φ \to y = w)) \leftrightarrow \exists z \in A \exists w \in B \forall x \in A \forall y \in B (φ \to (x = z \land y = w)))$
64	11 63	anbi12d	$⊢ (A \neq \emptyset \land B \neq \emptyset) \to (((\exists x \in A \exists y \in B φ \land \exists y \in B \exists x \in A φ) \land (\exists z \in A \forall x \in A (\exists y \in B φ \to x = z) \land \exists w \in B \forall y \in B (\exists x \in A φ \to y = w))) \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))))$
65	4 6 64	3bitrd	$⊢ (A \neq \emptyset \land B \neq \emptyset) \to ((\exists! x \in A \exists y \in B φ \land \exists! y \in B \exists x \in A φ) \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 2reu4lem

Proof