Theorem 2reu4a 39838

Description: Definition of double restricted existential uniqueness ("exactly one 𝑥 and exactly one 𝑦"), analogous to 2eu4 2544 with the additional requirement that the restricting classes are not empty (which is not necessary as shown in 2reu4 39839). (Contributed by Alexander van der Vekens, 1-Jul-2017.)

Assertion

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

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

Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem 2reu4a

Step	Hyp	Ref	Expression
1		reu3 3363	. . . 4 ⊢ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧)))
2		reu3 3363	. . . 4 ⊢ (∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)))
3	1, 2	anbi12i 729	. . 3 ⊢ ((∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧)) ∧ (∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
4	3	a1i 11	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧)) ∧ (∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)))))
5		an4 861	. . 3 ⊢ (((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧)) ∧ (∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))) ↔ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ∧ (∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
6	5	a1i 11	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧)) ∧ (∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))) ↔ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ∧ (∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)))))
7		rexcom 3080	. . . . . 6 ⊢ (∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
8	7	anbi2i 726	. . . . 5 ⊢ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑))
9		anidm 674	. . . . 5 ⊢ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
10	8, 9	bitri 263	. . . 4 ⊢ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
11	10	a1i 11	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑))
12		r19.26 3046	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
13		nfra1 2925	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)
14	13	r19.3rz 4014	. . . . . . . . . . . . 13 ⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤) ↔ ∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
15	14	bicomd 212	. . . . . . . . . . . 12 ⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
16	15	adantr 480	. . . . . . . . . . 11 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
17	16	adantr 480	. . . . . . . . . 10 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
18	17	anbi2d 736	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤))))
19		jcab 903	. . . . . . . . . . . . . 14 ⊢ ((𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ((𝜑 → 𝑥 = 𝑧) ∧ (𝜑 → 𝑦 = 𝑤)))
20	19	ralbii 2963	. . . . . . . . . . . . 13 ⊢ (∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑦 ∈ 𝐵 ((𝜑 → 𝑥 = 𝑧) ∧ (𝜑 → 𝑦 = 𝑤)))
21		r19.26 3046	. . . . . . . . . . . . 13 ⊢ (∀𝑦 ∈ 𝐵 ((𝜑 → 𝑥 = 𝑧) ∧ (𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
22	20, 21	bitri 263	. . . . . . . . . . . 12 ⊢ (∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
23	22	ralbii 2963	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
24		r19.26 3046	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
25	23, 24	bitri 263	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
26	25	a1i 11	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤))))
27	18, 26	bitr4d 270	. . . . . . . 8 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))
28	12, 27	syl5rbb 272	. . . . . . 7 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤))))
29		r19.26 3046	. . . . . . . . 9 ⊢ (∀𝑦 ∈ 𝐵 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑦 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)))
30		nfra1 2925	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧)
31	30	r19.3rz 4014	. . . . . . . . . . . 12 ⊢ (𝐵 ≠ ∅ → (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ↔ ∀𝑦 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧)))
32	31	ad2antlr 759	. . . . . . . . . . 11 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ↔ ∀𝑦 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧)))
33	32	bicomd 212	. . . . . . . . . 10 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑦 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ↔ ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧)))
34		ralcom 3079	. . . . . . . . . . 11 ⊢ (∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤))
35	34	a1i 11	. . . . . . . . . 10 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
36	33, 35	anbi12d 743	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → ((∀𝑦 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤))))
37	29, 36	syl5bb 271	. . . . . . . 8 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑦 ∈ 𝐵 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤))))
38	37	ralbidv 2969	. . . . . . 7 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)) ↔ ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤))))
39	28, 38	bitr4d 270	. . . . . 6 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤))))
40		r19.23v 3005	. . . . . . . . 9 ⊢ (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ↔ (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧))
41		r19.23v 3005	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))
42	40, 41	anbi12i 729	. . . . . . . 8 ⊢ ((∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)) ↔ ((∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)))
43	42	2ralbii 2964	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)))
44	43	a1i 11	. . . . . 6 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
45		df-ne 2782	. . . . . . . . . . . 12 ⊢ (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅)
46	45	biimpi 205	. . . . . . . . . . 11 ⊢ (𝐴 ≠ ∅ → ¬ 𝐴 = ∅)
47		df-ne 2782	. . . . . . . . . . . 12 ⊢ (𝐵 ≠ ∅ ↔ ¬ 𝐵 = ∅)
48	47	biimpi 205	. . . . . . . . . . 11 ⊢ (𝐵 ≠ ∅ → ¬ 𝐵 = ∅)
49	46, 48	anim12i 588	. . . . . . . . . 10 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅))
50	49	olcd 407	. . . . . . . . 9 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅)))
51		dfbi3 933	. . . . . . . . 9 ⊢ ((𝐴 = ∅ ↔ 𝐵 = ∅) ↔ ((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅)))
52	50, 51	sylibr 223	. . . . . . . 8 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (𝐴 = ∅ ↔ 𝐵 = ∅))
53		nfre1 2988	. . . . . . . . . 10 ⊢ Ⅎ𝑦∃𝑦 ∈ 𝐵 𝜑
54		nfv 1830	. . . . . . . . . 10 ⊢ Ⅎ𝑦 𝑥 = 𝑧
55	53, 54	nfim 1813	. . . . . . . . 9 ⊢ Ⅎ𝑦(∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧)
56		nfre1 2988	. . . . . . . . . 10 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝜑
57		nfv 1830	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝑦 = 𝑤
58	56, 57	nfim 1813	. . . . . . . . 9 ⊢ Ⅎ𝑥(∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)
59	55, 58	raaan2 39824	. . . . . . . 8 ⊢ ((𝐴 = ∅ ↔ 𝐵 = ∅) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
60	52, 59	syl 17	. . . . . . 7 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
61	60	adantr 480	. . . . . 6 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
62	39, 44, 61	3bitrd 293	. . . . 5 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
63	62	2rexbidva 3038	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 (∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
64		reeanv 3086	. . . 4 ⊢ (∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 (∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)) ↔ (∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)))
65	63, 64	syl6rbb 276	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)) ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))
66	11, 65	anbi12d 743	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ∧ (∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))) ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))))
67	4, 6, 66	3bitrd 293	1 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  ∃!wreu 2898  ∅c0 3874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-v 3175  df-dif 3543  df-nul 3875

This theorem is referenced by:  2reu4  39839