Theorem 2reu4lem 4522

Description: Lemma for 2reu4 4523. (Contributed by Alexander van der Vekens, 1-Jul-2017.)

Assertion

Ref	Expression
2reu4lem	⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))))

Distinct variable groups:   𝑧,𝑤,𝜑   𝑥,𝑤,𝑦,𝐴,𝑧   𝑤,𝐵,𝑥,𝑦,𝑧

Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem 2reu4lem

Step	Hyp	Ref	Expression
1		reu3 3733	. . . 4 ⊢ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧)))
2		reu3 3733	. . . 4 ⊢ (∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)))
3	1, 2	anbi12i 628	. . 3 ⊢ ((∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧)) ∧ (∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
4	3	a1i 11	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧)) ∧ (∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)))))
5		an4 656	. . 3 ⊢ (((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧)) ∧ (∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))) ↔ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ∧ (∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
6	5	a1i 11	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧)) ∧ (∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))) ↔ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ∧ (∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)))))
7		rexcom 3290	. . . . . 6 ⊢ (∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
8	7	anbi2i 623	. . . . 5 ⊢ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑))
9		anidm 564	. . . . 5 ⊢ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
10	8, 9	bitri 275	. . . 4 ⊢ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
11	10	a1i 11	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑))
12		r19.26 3111	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
13		nfra1 3284	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)
14	13	r19.3rz 4497	. . . . . . . . . . . . 13 ⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤) ↔ ∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
15	14	bicomd 223	. . . . . . . . . . . 12 ⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
16	15	adantr 480	. . . . . . . . . . 11 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
17	16	adantr 480	. . . . . . . . . 10 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
18	17	anbi2d 630	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤))))
19		jcab 517	. . . . . . . . . . . . . 14 ⊢ ((𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ((𝜑 → 𝑥 = 𝑧) ∧ (𝜑 → 𝑦 = 𝑤)))
20	19	ralbii 3093	. . . . . . . . . . . . 13 ⊢ (∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑦 ∈ 𝐵 ((𝜑 → 𝑥 = 𝑧) ∧ (𝜑 → 𝑦 = 𝑤)))
21		r19.26 3111	. . . . . . . . . . . . 13 ⊢ (∀𝑦 ∈ 𝐵 ((𝜑 → 𝑥 = 𝑧) ∧ (𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
22	20, 21	bitri 275	. . . . . . . . . . . 12 ⊢ (∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
23	22	ralbii 3093	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
24		r19.26 3111	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
25	23, 24	bitri 275	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
26	25	a1i 11	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤))))
27	18, 26	bitr4d 282	. . . . . . . 8 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))
28	12, 27	bitr2id 284	. . . . . . 7 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤))))
29		r19.26 3111	. . . . . . . . 9 ⊢ (∀𝑦 ∈ 𝐵 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑦 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)))
30		nfra1 3284	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧)
31	30	r19.3rz 4497	. . . . . . . . . . . 12 ⊢ (𝐵 ≠ ∅ → (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ↔ ∀𝑦 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧)))
32	31	ad2antlr 727	. . . . . . . . . . 11 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ↔ ∀𝑦 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧)))
33	32	bicomd 223	. . . . . . . . . 10 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑦 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ↔ ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧)))
34		ralcom 3289	. . . . . . . . . . 11 ⊢ (∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤))
35	34	a1i 11	. . . . . . . . . 10 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
36	33, 35	anbi12d 632	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → ((∀𝑦 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤))))
37	29, 36	bitrid 283	. . . . . . . 8 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑦 ∈ 𝐵 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤))))
38	37	ralbidv 3178	. . . . . . 7 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)) ↔ ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤))))
39	28, 38	bitr4d 282	. . . . . 6 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤))))
40		r19.23v 3183	. . . . . . . . 9 ⊢ (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ↔ (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧))
41		r19.23v 3183	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))
42	40, 41	anbi12i 628	. . . . . . . 8 ⊢ ((∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)) ↔ ((∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)))
43	42	2ralbii 3128	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)))
44	43	a1i 11	. . . . . 6 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
45		neneq 2946	. . . . . . . . . . 11 ⊢ (𝐴 ≠ ∅ → ¬ 𝐴 = ∅)
46		neneq 2946	. . . . . . . . . . 11 ⊢ (𝐵 ≠ ∅ → ¬ 𝐵 = ∅)
47	45, 46	anim12i 613	. . . . . . . . . 10 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅))
48	47	olcd 875	. . . . . . . . 9 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅)))
49		dfbi3 1050	. . . . . . . . 9 ⊢ ((𝐴 = ∅ ↔ 𝐵 = ∅) ↔ ((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅)))
50	48, 49	sylibr 234	. . . . . . . 8 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (𝐴 = ∅ ↔ 𝐵 = ∅))
51		nfre1 3285	. . . . . . . . . 10 ⊢ Ⅎ𝑦∃𝑦 ∈ 𝐵 𝜑
52		nfv 1914	. . . . . . . . . 10 ⊢ Ⅎ𝑦 𝑥 = 𝑧
53	51, 52	nfim 1896	. . . . . . . . 9 ⊢ Ⅎ𝑦(∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧)
54		nfre1 3285	. . . . . . . . . 10 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝜑
55		nfv 1914	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝑦 = 𝑤
56	54, 55	nfim 1896	. . . . . . . . 9 ⊢ Ⅎ𝑥(∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)
57	53, 56	raaan2 4521	. . . . . . . 8 ⊢ ((𝐴 = ∅ ↔ 𝐵 = ∅) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
58	50, 57	syl 17	. . . . . . 7 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
59	58	adantr 480	. . . . . 6 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
60	39, 44, 59	3bitrd 305	. . . . 5 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
61	60	2rexbidva 3220	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 (∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
62		reeanv 3229	. . . 4 ⊢ (∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 (∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)) ↔ (∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)))
63	61, 62	bitr2di 288	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)) ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))
64	11, 63	anbi12d 632	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ∧ (∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))) ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))))
65	4, 6, 64	3bitrd 305	1 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   = wceq 1540   ∈ wcel 2108   ≠ wne 2940  ∀wral 3061  ∃wrex 3070  ∃!wreu 3378  ∅c0 4333

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-dif 3954  df-nul 4334

This theorem is referenced by:  2reu4  4523