Theorem 2reu4a 41189

Description: Definition of double restricted existential uniqueness ("exactly one 𝑥 and exactly one 𝑦"), analogous to 2eu4 2556 with the additional requirement that the restricting classes are not empty (which is not necessary as shown in 2reu4 41190). (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 3396	. . . 4 ⊢ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧)))
2		reu3 3396	. . . 4 ⊢ (∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)))
3	1, 2	anbi12i 733	. . 3 ⊢ ((∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧)) ∧ (∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
4	3	a1i 11	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧)) ∧ (∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)))))
5		an4 865	. . 3 ⊢ (((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧)) ∧ (∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))) ↔ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ∧ (∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
6	5	a1i 11	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧)) ∧ (∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))) ↔ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ∧ (∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)))))
7		rexcom 3099	. . . . . 6 ⊢ (∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
8	7	anbi2i 730	. . . . 5 ⊢ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑))
9		anidm 676	. . . . 5 ⊢ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
10	8, 9	bitri 264	. . . 4 ⊢ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)
11	10	a1i 11	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑))
12		r19.26 3064	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
13		nfra1 2941	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)
14	13	r19.3rz 4062	. . . . . . . . . . . . 13 ⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤) ↔ ∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
15	14	bicomd 213	. . . . . . . . . . . 12 ⊢ (𝐴 ≠ ∅ → (∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
16	15	adantr 481	. . . . . . . . . . 11 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
17	16	adantr 481	. . . . . . . . . 10 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
18	17	anbi2d 740	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤))))
19		jcab 907	. . . . . . . . . . . . . 14 ⊢ ((𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ((𝜑 → 𝑥 = 𝑧) ∧ (𝜑 → 𝑦 = 𝑤)))
20	19	ralbii 2980	. . . . . . . . . . . . 13 ⊢ (∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑦 ∈ 𝐵 ((𝜑 → 𝑥 = 𝑧) ∧ (𝜑 → 𝑦 = 𝑤)))
21		r19.26 3064	. . . . . . . . . . . . 13 ⊢ (∀𝑦 ∈ 𝐵 ((𝜑 → 𝑥 = 𝑧) ∧ (𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
22	20, 21	bitri 264	. . . . . . . . . . . 12 ⊢ (∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
23	22	ralbii 2980	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
24		r19.26 3064	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
25	23, 24	bitri 264	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
26	25	a1i 11	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤))))
27	18, 26	bitr4d 271	. . . . . . . 8 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))
28	12, 27	syl5rbb 273	. . . . . . 7 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤))))
29		r19.26 3064	. . . . . . . . 9 ⊢ (∀𝑦 ∈ 𝐵 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑦 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)))
30		nfra1 2941	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧)
31	30	r19.3rz 4062	. . . . . . . . . . . 12 ⊢ (𝐵 ≠ ∅ → (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ↔ ∀𝑦 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧)))
32	31	ad2antlr 763	. . . . . . . . . . 11 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ↔ ∀𝑦 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧)))
33	32	bicomd 213	. . . . . . . . . 10 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑦 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ↔ ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧)))
34		ralcom 3098	. . . . . . . . . . 11 ⊢ (∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤))
35	34	a1i 11	. . . . . . . . . 10 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤)))
36	33, 35	anbi12d 747	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → ((∀𝑦 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤))))
37	29, 36	syl5bb 272	. . . . . . . 8 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑦 ∈ 𝐵 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤))))
38	37	ralbidv 2986	. . . . . . 7 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)) ↔ ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑦 = 𝑤))))
39	28, 38	bitr4d 271	. . . . . 6 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤))))
40		r19.23v 3023	. . . . . . . . 9 ⊢ (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ↔ (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧))
41		r19.23v 3023	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))
42	40, 41	anbi12i 733	. . . . . . . 8 ⊢ ((∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)) ↔ ((∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)))
43	42	2ralbii 2981	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)))
44	43	a1i 11	. . . . . 6 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝑧) ∧ ∀𝑥 ∈ 𝐴 (𝜑 → 𝑦 = 𝑤)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
45		neneq 2800	. . . . . . . . . . 11 ⊢ (𝐴 ≠ ∅ → ¬ 𝐴 = ∅)
46		neneq 2800	. . . . . . . . . . 11 ⊢ (𝐵 ≠ ∅ → ¬ 𝐵 = ∅)
47	45, 46	anim12i 590	. . . . . . . . . 10 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅))
48	47	olcd 408	. . . . . . . . 9 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅)))
49		dfbi3 994	. . . . . . . . 9 ⊢ ((𝐴 = ∅ ↔ 𝐵 = ∅) ↔ ((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅)))
50	48, 49	sylibr 224	. . . . . . . 8 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (𝐴 = ∅ ↔ 𝐵 = ∅))
51		nfre1 3005	. . . . . . . . . 10 ⊢ Ⅎ𝑦∃𝑦 ∈ 𝐵 𝜑
52		nfv 1843	. . . . . . . . . 10 ⊢ Ⅎ𝑦 𝑥 = 𝑧
53	51, 52	nfim 1825	. . . . . . . . 9 ⊢ Ⅎ𝑦(∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧)
54		nfre1 3005	. . . . . . . . . 10 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝜑
55		nfv 1843	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝑦 = 𝑤
56	54, 55	nfim 1825	. . . . . . . . 9 ⊢ Ⅎ𝑥(∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)
57	53, 56	raaan2 41175	. . . . . . . 8 ⊢ ((𝐴 = ∅ ↔ 𝐵 = ∅) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
58	50, 57	syl 17	. . . . . . 7 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
59	58	adantr 481	. . . . . 6 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
60	39, 44, 59	3bitrd 294	. . . . 5 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ (∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
61	60	2rexbidva 3056	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 (∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))))
62		reeanv 3107	. . . 4 ⊢ (∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 (∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)) ↔ (∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)))
63	61, 62	syl6rbb 277	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤)) ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))
64	11, 63	anbi12d 747	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ∧ (∃𝑧 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐵 𝜑 → 𝑥 = 𝑧) ∧ ∃𝑤 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑥 ∈ 𝐴 𝜑 → 𝑦 = 𝑤))) ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))))
65	4, 6, 64	3bitrd 294	1 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 383   ∧ wa 384   = wceq 1483   ∈ wcel 1990   ≠ wne 2794  ∀wral 2912  ∃wrex 2913  ∃!wreu 2914  ∅c0 3915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-v 3202  df-dif 3577  df-nul 3916

This theorem is referenced by:  2reu4  41190