Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  2reu4a Structured version   Visualization version   GIF version

Theorem 2reu4a 41713
Description: Definition of double restricted existential uniqueness ("exactly one 𝑥 and exactly one 𝑦"), analogous to 2eu4 2694 with the additional requirement that the restricting classes are not empty (which is not necessary as shown in 2reu4 41714). (Contributed by Alexander van der Vekens, 1-Jul-2017.)
Assertion
Ref Expression
2reu4a ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃!𝑥𝐴𝑦𝐵 𝜑 ∧ ∃!𝑦𝐵𝑥𝐴 𝜑) ↔ (∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑧𝐴𝑤𝐵𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)))))
Distinct variable groups:   𝑧,𝑤,𝜑   𝑥,𝑤,𝑦,𝐴,𝑧   𝑤,𝐵,𝑥,𝑦,𝑧
Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem 2reu4a
StepHypRef Expression
1 reu3 3537 . . . 4 (∃!𝑥𝐴𝑦𝐵 𝜑 ↔ (∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧)))
2 reu3 3537 . . . 4 (∃!𝑦𝐵𝑥𝐴 𝜑 ↔ (∃𝑦𝐵𝑥𝐴 𝜑 ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤)))
31, 2anbi12i 735 . . 3 ((∃!𝑥𝐴𝑦𝐵 𝜑 ∧ ∃!𝑦𝐵𝑥𝐴 𝜑) ↔ ((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧)) ∧ (∃𝑦𝐵𝑥𝐴 𝜑 ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))))
43a1i 11 . 2 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃!𝑥𝐴𝑦𝐵 𝜑 ∧ ∃!𝑦𝐵𝑥𝐴 𝜑) ↔ ((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧)) ∧ (∃𝑦𝐵𝑥𝐴 𝜑 ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤)))))
5 an4 900 . . 3 (((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧)) ∧ (∃𝑦𝐵𝑥𝐴 𝜑 ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))) ↔ ((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑦𝐵𝑥𝐴 𝜑) ∧ (∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))))
65a1i 11 . 2 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧)) ∧ (∃𝑦𝐵𝑥𝐴 𝜑 ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))) ↔ ((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑦𝐵𝑥𝐴 𝜑) ∧ (∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤)))))
7 rexcom 3237 . . . . . 6 (∃𝑦𝐵𝑥𝐴 𝜑 ↔ ∃𝑥𝐴𝑦𝐵 𝜑)
87anbi2i 732 . . . . 5 ((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑦𝐵𝑥𝐴 𝜑) ↔ (∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑥𝐴𝑦𝐵 𝜑))
9 anidm 679 . . . . 5 ((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑥𝐴𝑦𝐵 𝜑) ↔ ∃𝑥𝐴𝑦𝐵 𝜑)
108, 9bitri 264 . . . 4 ((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑦𝐵𝑥𝐴 𝜑) ↔ ∃𝑥𝐴𝑦𝐵 𝜑)
1110a1i 11 . . 3 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑦𝐵𝑥𝐴 𝜑) ↔ ∃𝑥𝐴𝑦𝐵 𝜑))
12 r19.26 3202 . . . . . . . 8 (∀𝑥𝐴 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)) ↔ (∀𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)))
13 nfra1 3079 . . . . . . . . . . . . . 14 𝑥𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)
1413r19.3rz 4206 . . . . . . . . . . . . 13 (𝐴 ≠ ∅ → (∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤) ↔ ∀𝑥𝐴𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)))
1514bicomd 213 . . . . . . . . . . . 12 (𝐴 ≠ ∅ → (∀𝑥𝐴𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤) ↔ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)))
1615adantr 472 . . . . . . . . . . 11 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (∀𝑥𝐴𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤) ↔ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)))
1716adantr 472 . . . . . . . . . 10 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑥𝐴𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤) ↔ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)))
1817anbi2d 742 . . . . . . . . 9 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → ((∀𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)) ↔ (∀𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤))))
19 jcab 943 . . . . . . . . . . . . . 14 ((𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ ((𝜑𝑥 = 𝑧) ∧ (𝜑𝑦 = 𝑤)))
2019ralbii 3118 . . . . . . . . . . . . 13 (∀𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ ∀𝑦𝐵 ((𝜑𝑥 = 𝑧) ∧ (𝜑𝑦 = 𝑤)))
21 r19.26 3202 . . . . . . . . . . . . 13 (∀𝑦𝐵 ((𝜑𝑥 = 𝑧) ∧ (𝜑𝑦 = 𝑤)) ↔ (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (𝜑𝑦 = 𝑤)))
2220, 21bitri 264 . . . . . . . . . . . 12 (∀𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (𝜑𝑦 = 𝑤)))
2322ralbii 3118 . . . . . . . . . . 11 (∀𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ ∀𝑥𝐴 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (𝜑𝑦 = 𝑤)))
24 r19.26 3202 . . . . . . . . . . 11 (∀𝑥𝐴 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (𝜑𝑦 = 𝑤)) ↔ (∀𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)))
2523, 24bitri 264 . . . . . . . . . 10 (∀𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ (∀𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)))
2625a1i 11 . . . . . . . . 9 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ (∀𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤))))
2718, 26bitr4d 271 . . . . . . . 8 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → ((∀𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)) ↔ ∀𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤))))
2812, 27syl5rbb 273 . . . . . . 7 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ ∀𝑥𝐴 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤))))
29 r19.26 3202 . . . . . . . . 9 (∀𝑦𝐵 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴 (𝜑𝑦 = 𝑤)) ↔ (∀𝑦𝐵𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵𝑥𝐴 (𝜑𝑦 = 𝑤)))
30 nfra1 3079 . . . . . . . . . . . . 13 𝑦𝑦𝐵 (𝜑𝑥 = 𝑧)
3130r19.3rz 4206 . . . . . . . . . . . 12 (𝐵 ≠ ∅ → (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ↔ ∀𝑦𝐵𝑦𝐵 (𝜑𝑥 = 𝑧)))
3231ad2antlr 765 . . . . . . . . . . 11 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ↔ ∀𝑦𝐵𝑦𝐵 (𝜑𝑥 = 𝑧)))
3332bicomd 213 . . . . . . . . . 10 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑦𝐵𝑦𝐵 (𝜑𝑥 = 𝑧) ↔ ∀𝑦𝐵 (𝜑𝑥 = 𝑧)))
34 ralcom 3236 . . . . . . . . . . 11 (∀𝑦𝐵𝑥𝐴 (𝜑𝑦 = 𝑤) ↔ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤))
3534a1i 11 . . . . . . . . . 10 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑦𝐵𝑥𝐴 (𝜑𝑦 = 𝑤) ↔ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)))
3633, 35anbi12d 749 . . . . . . . . 9 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → ((∀𝑦𝐵𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵𝑥𝐴 (𝜑𝑦 = 𝑤)) ↔ (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤))))
3729, 36syl5bb 272 . . . . . . . 8 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑦𝐵 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴 (𝜑𝑦 = 𝑤)) ↔ (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤))))
3837ralbidv 3124 . . . . . . 7 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑥𝐴𝑦𝐵 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴 (𝜑𝑦 = 𝑤)) ↔ ∀𝑥𝐴 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤))))
3928, 38bitr4d 271 . . . . . 6 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ ∀𝑥𝐴𝑦𝐵 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴 (𝜑𝑦 = 𝑤))))
40 r19.23v 3161 . . . . . . . . 9 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ↔ (∃𝑦𝐵 𝜑𝑥 = 𝑧))
41 r19.23v 3161 . . . . . . . . 9 (∀𝑥𝐴 (𝜑𝑦 = 𝑤) ↔ (∃𝑥𝐴 𝜑𝑦 = 𝑤))
4240, 41anbi12i 735 . . . . . . . 8 ((∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴 (𝜑𝑦 = 𝑤)) ↔ ((∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ (∃𝑥𝐴 𝜑𝑦 = 𝑤)))
43422ralbii 3119 . . . . . . 7 (∀𝑥𝐴𝑦𝐵 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴 (𝜑𝑦 = 𝑤)) ↔ ∀𝑥𝐴𝑦𝐵 ((∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ (∃𝑥𝐴 𝜑𝑦 = 𝑤)))
4443a1i 11 . . . . . 6 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑥𝐴𝑦𝐵 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴 (𝜑𝑦 = 𝑤)) ↔ ∀𝑥𝐴𝑦𝐵 ((∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ (∃𝑥𝐴 𝜑𝑦 = 𝑤))))
45 neneq 2938 . . . . . . . . . . 11 (𝐴 ≠ ∅ → ¬ 𝐴 = ∅)
46 neneq 2938 . . . . . . . . . . 11 (𝐵 ≠ ∅ → ¬ 𝐵 = ∅)
4745, 46anim12i 591 . . . . . . . . . 10 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅))
4847olcd 407 . . . . . . . . 9 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅)))
49 dfbi3 1036 . . . . . . . . 9 ((𝐴 = ∅ ↔ 𝐵 = ∅) ↔ ((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅)))
5048, 49sylibr 224 . . . . . . . 8 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (𝐴 = ∅ ↔ 𝐵 = ∅))
51 nfre1 3143 . . . . . . . . . 10 𝑦𝑦𝐵 𝜑
52 nfv 1992 . . . . . . . . . 10 𝑦 𝑥 = 𝑧
5351, 52nfim 1974 . . . . . . . . 9 𝑦(∃𝑦𝐵 𝜑𝑥 = 𝑧)
54 nfre1 3143 . . . . . . . . . 10 𝑥𝑥𝐴 𝜑
55 nfv 1992 . . . . . . . . . 10 𝑥 𝑦 = 𝑤
5654, 55nfim 1974 . . . . . . . . 9 𝑥(∃𝑥𝐴 𝜑𝑦 = 𝑤)
5753, 56raaan2 41699 . . . . . . . 8 ((𝐴 = ∅ ↔ 𝐵 = ∅) → (∀𝑥𝐴𝑦𝐵 ((∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ (∃𝑥𝐴 𝜑𝑦 = 𝑤)) ↔ (∀𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))))
5850, 57syl 17 . . . . . . 7 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (∀𝑥𝐴𝑦𝐵 ((∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ (∃𝑥𝐴 𝜑𝑦 = 𝑤)) ↔ (∀𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))))
5958adantr 472 . . . . . 6 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑥𝐴𝑦𝐵 ((∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ (∃𝑥𝐴 𝜑𝑦 = 𝑤)) ↔ (∀𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))))
6039, 44, 593bitrd 294 . . . . 5 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ (∀𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))))
61602rexbidva 3194 . . . 4 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (∃𝑧𝐴𝑤𝐵𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ ∃𝑧𝐴𝑤𝐵 (∀𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))))
62 reeanv 3245 . . . 4 (∃𝑧𝐴𝑤𝐵 (∀𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤)) ↔ (∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤)))
6361, 62syl6rbb 277 . . 3 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤)) ↔ ∃𝑧𝐴𝑤𝐵𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤))))
6411, 63anbi12d 749 . 2 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑦𝐵𝑥𝐴 𝜑) ∧ (∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))) ↔ (∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑧𝐴𝑤𝐵𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)))))
654, 6, 643bitrd 294 1 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃!𝑥𝐴𝑦𝐵 𝜑 ∧ ∃!𝑦𝐵𝑥𝐴 𝜑) ↔ (∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑧𝐴𝑤𝐵𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383   = wceq 1632  wcel 2139  wne 2932  wral 3050  wrex 3051  ∃!wreu 3052  c0 4058
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-v 3342  df-dif 3718  df-nul 4059
This theorem is referenced by:  2reu4  41714
  Copyright terms: Public domain W3C validator