Theorem 2reu4lem 4456

Description: Lemma for 2reu4 4457. (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 3662	. . . 4 ⊢ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧)))
2		reu3 3662	. . . 4 ⊢ (∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)))
3	1, 2	anbi12i 627	. . 3 ⊢ ((∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧)) ∧ (∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
4	3	a1i 11	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧)) ∧ (∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)))))
5		an4 653	. . 3 ⊢ (((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧)) ∧ (∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))) ↔ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ∧ (∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
6	5	a1i 11	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧)) ∧ (∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))) ↔ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ∧ (∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)))))
7		rexcom 3234	. . . . . 6 ⊢ (∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
8	7	anbi2i 623	. . . . 5 ⊢ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑))
9		anidm 565	. . . . 5 ⊢ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
10	8, 9	bitri 274	. . . 4 ⊢ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
11	10	a1i 11	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑))
12		r19.26 3095	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
13		nfra1 3144	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)
14	13	r19.3rz 4427	. . . . . . . . . . . . 13 ⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤) ↔ ∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
15	14	bicomd 222	. . . . . . . . . . . 12 ⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
16	15	adantr 481	. . . . . . . . . . 11 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
17	16	adantr 481	. . . . . . . . . 10 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
18	17	anbi2d 629	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤))))
19		jcab 518	. . . . . . . . . . . . . 14 ⊢ ((𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ((𝜑 → 𝑥 = 𝑧) ∧ (𝜑 → 𝑦 = 𝑤)))
20	19	ralbii 3092	. . . . . . . . . . . . 13 ⊢ (∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑦 ∈ 𝐵 ((𝜑 → 𝑥 = 𝑧) ∧ (𝜑 → 𝑦 = 𝑤)))
21		r19.26 3095	. . . . . . . . . . . . 13 ⊢ (∀𝑦 ∈ 𝐵 ((𝜑 → 𝑥 = 𝑧) ∧ (𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
22	20, 21	bitri 274	. . . . . . . . . . . 12 ⊢ (∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
23	22	ralbii 3092	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
24		r19.26 3095	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
25	23, 24	bitri 274	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
26	25	a1i 11	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤))))
27	18, 26	bitr4d 281	. . . . . . . 8 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))
28	12, 27	bitr2id 284	. . . . . . 7 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤))))
29		r19.26 3095	. . . . . . . . 9 ⊢ (∀𝑦 ∈ 𝐵 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑦 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)))
30		nfra1 3144	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧)
31	30	r19.3rz 4427	. . . . . . . . . . . 12 ⊢ (𝐵 ≠ ∅ → (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ↔ ∀𝑦 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧)))
32	31	ad2antlr 724	. . . . . . . . . . 11 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ↔ ∀𝑦 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧)))
33	32	bicomd 222	. . . . . . . . . 10 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑦 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ↔ ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧)))
34		ralcom 3166	. . . . . . . . . . 11 ⊢ (∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤))
35	34	a1i 11	. . . . . . . . . 10 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
36	33, 35	anbi12d 631	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → ((∀𝑦 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤))))
37	29, 36	bitrid 282	. . . . . . . 8 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑦 ∈ 𝐵 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤))))
38	37	ralbidv 3112	. . . . . . 7 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)) ↔ ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤))))
39	28, 38	bitr4d 281	. . . . . 6 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤))))
40		r19.23v 3208	. . . . . . . . 9 ⊢ (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ↔ (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧))
41		r19.23v 3208	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))
42	40, 41	anbi12i 627	. . . . . . . 8 ⊢ ((∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)) ↔ ((∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)))
43	42	2ralbii 3093	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)))
44	43	a1i 11	. . . . . 6 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
45		neneq 2949	. . . . . . . . . . 11 ⊢ (𝐴 ≠ ∅ → ¬ 𝐴 = ∅)
46		neneq 2949	. . . . . . . . . . 11 ⊢ (𝐵 ≠ ∅ → ¬ 𝐵 = ∅)
47	45, 46	anim12i 613	. . . . . . . . . 10 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅))
48	47	olcd 871	. . . . . . . . 9 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅)))
49		dfbi3 1047	. . . . . . . . 9 ⊢ ((𝐴 = ∅ ↔ 𝐵 = ∅) ↔ ((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅)))
50	48, 49	sylibr 233	. . . . . . . 8 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (𝐴 = ∅ ↔ 𝐵 = ∅))
51		nfre1 3239	. . . . . . . . . 10 ⊢ Ⅎ𝑦∃𝑦 ∈ 𝐵 𝜑
52		nfv 1917	. . . . . . . . . 10 ⊢ Ⅎ𝑦 𝑥 = 𝑧
53	51, 52	nfim 1899	. . . . . . . . 9 ⊢ Ⅎ𝑦(∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧)
54		nfre1 3239	. . . . . . . . . 10 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝜑
55		nfv 1917	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝑦 = 𝑤
56	54, 55	nfim 1899	. . . . . . . . 9 ⊢ Ⅎ𝑥(∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)
57	53, 56	raaan2 4455	. . . . . . . 8 ⊢ ((𝐴 = ∅ ↔ 𝐵 = ∅) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
58	50, 57	syl 17	. . . . . . 7 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
59	58	adantr 481	. . . . . 6 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
60	39, 44, 59	3bitrd 305	. . . . 5 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
61	60	2rexbidva 3228	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 (∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
62		reeanv 3294	. . . 4 ⊢ (∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 (∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)) ↔ (∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)))
63	61, 62	bitr2di 288	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)) ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))
64	11, 63	anbi12d 631	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ∧ (∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))) ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))))
65	4, 6, 64	3bitrd 305	1 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 844   = wceq 1539   ∈ wcel 2106   ≠ wne 2943  ∀wral 3064  ∃wrex 3065  ∃!wreu 3066  ∅c0 4256

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-dif 3890  df-nul 4257

This theorem is referenced by:  2reu4  4457