Theorem 2reu4a 42014

Description: Definition of double restricted existential uniqueness ("exactly one 𝑥 and exactly one 𝑦"), analogous to 2eu4 2736 with the additional requirement that the restricting classes are not empty (which is not necessary as shown in 2reu4 42015). (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 3621	. . . 4 ⊢ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧)))
2		reu3 3621	. . . 4 ⊢ (∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)))
3	1, 2	anbi12i 622	. . 3 ⊢ ((∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧)) ∧ (∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
4	3	a1i 11	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧)) ∧ (∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)))))
5		an4 648	. . 3 ⊢ (((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧)) ∧ (∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))) ↔ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ∧ (∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
6	5	a1i 11	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧)) ∧ (∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))) ↔ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ∧ (∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)))))
7		rexcom 3309	. . . . . 6 ⊢ (∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
8	7	anbi2i 618	. . . . 5 ⊢ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑))
9		anidm 562	. . . . 5 ⊢ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
10	8, 9	bitri 267	. . . 4 ⊢ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
11	10	a1i 11	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑))
12		r19.26 3274	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
13		nfra1 3150	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)
14	13	r19.3rz 4284	. . . . . . . . . . . . 13 ⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤) ↔ ∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
15	14	bicomd 215	. . . . . . . . . . . 12 ⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
16	15	adantr 474	. . . . . . . . . . 11 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
17	16	adantr 474	. . . . . . . . . 10 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
18	17	anbi2d 624	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤))))
19		jcab 515	. . . . . . . . . . . . . 14 ⊢ ((𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ((𝜑 → 𝑥 = 𝑧) ∧ (𝜑 → 𝑦 = 𝑤)))
20	19	ralbii 3189	. . . . . . . . . . . . 13 ⊢ (∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑦 ∈ 𝐵 ((𝜑 → 𝑥 = 𝑧) ∧ (𝜑 → 𝑦 = 𝑤)))
21		r19.26 3274	. . . . . . . . . . . . 13 ⊢ (∀𝑦 ∈ 𝐵 ((𝜑 → 𝑥 = 𝑧) ∧ (𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
22	20, 21	bitri 267	. . . . . . . . . . . 12 ⊢ (∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
23	22	ralbii 3189	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
24		r19.26 3274	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
25	23, 24	bitri 267	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
26	25	a1i 11	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤))))
27	18, 26	bitr4d 274	. . . . . . . 8 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))
28	12, 27	syl5rbb 276	. . . . . . 7 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤))))
29		r19.26 3274	. . . . . . . . 9 ⊢ (∀𝑦 ∈ 𝐵 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑦 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)))
30		nfra1 3150	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧)
31	30	r19.3rz 4284	. . . . . . . . . . . 12 ⊢ (𝐵 ≠ ∅ → (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ↔ ∀𝑦 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧)))
32	31	ad2antlr 720	. . . . . . . . . . 11 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ↔ ∀𝑦 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧)))
33	32	bicomd 215	. . . . . . . . . 10 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑦 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ↔ ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧)))
34		ralcom 3308	. . . . . . . . . . 11 ⊢ (∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤))
35	34	a1i 11	. . . . . . . . . 10 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
36	33, 35	anbi12d 626	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → ((∀𝑦 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤))))
37	29, 36	syl5bb 275	. . . . . . . 8 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑦 ∈ 𝐵 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤))))
38	37	ralbidv 3195	. . . . . . 7 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)) ↔ ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤))))
39	28, 38	bitr4d 274	. . . . . 6 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤))))
40		r19.23v 3232	. . . . . . . . 9 ⊢ (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ↔ (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧))
41		r19.23v 3232	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))
42	40, 41	anbi12i 622	. . . . . . . 8 ⊢ ((∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)) ↔ ((∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)))
43	42	2ralbii 3190	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)))
44	43	a1i 11	. . . . . 6 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
45		neneq 3005	. . . . . . . . . . 11 ⊢ (𝐴 ≠ ∅ → ¬ 𝐴 = ∅)
46		neneq 3005	. . . . . . . . . . 11 ⊢ (𝐵 ≠ ∅ → ¬ 𝐵 = ∅)
47	45, 46	anim12i 608	. . . . . . . . . 10 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅))
48	47	olcd 907	. . . . . . . . 9 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅)))
49		dfbi3 1078	. . . . . . . . 9 ⊢ ((𝐴 = ∅ ↔ 𝐵 = ∅) ↔ ((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅)))
50	48, 49	sylibr 226	. . . . . . . 8 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (𝐴 = ∅ ↔ 𝐵 = ∅))
51		nfre1 3213	. . . . . . . . . 10 ⊢ Ⅎ𝑦∃𝑦 ∈ 𝐵 𝜑
52		nfv 2015	. . . . . . . . . 10 ⊢ Ⅎ𝑦 𝑥 = 𝑧
53	51, 52	nfim 2001	. . . . . . . . 9 ⊢ Ⅎ𝑦(∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧)
54		nfre1 3213	. . . . . . . . . 10 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝜑
55		nfv 2015	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝑦 = 𝑤
56	54, 55	nfim 2001	. . . . . . . . 9 ⊢ Ⅎ𝑥(∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)
57	53, 56	raaan2 41961	. . . . . . . 8 ⊢ ((𝐴 = ∅ ↔ 𝐵 = ∅) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
58	50, 57	syl 17	. . . . . . 7 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
59	58	adantr 474	. . . . . 6 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
60	39, 44, 59	3bitrd 297	. . . . 5 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
61	60	2rexbidva 3266	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 (∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
62		reeanv 3317	. . . 4 ⊢ (∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 (∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)) ↔ (∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)))
63	61, 62	syl6rbb 280	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)) ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))
64	11, 63	anbi12d 626	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ∧ (∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))) ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))))
65	4, 6, 64	3bitrd 297	1 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 386   ∨ wo 880   = wceq 1658   ∈ wcel 2166   ≠ wne 2999  ∀wral 3117  ∃wrex 3118  ∃!wreu 3119  ∅c0 4144

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-reu 3124  df-rmo 3125  df-v 3416  df-dif 3801  df-nul 4145

This theorem is referenced by:  2reu4  42015