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 40514
Description: Definition of double restricted existential uniqueness ("exactly one 𝑥 and exactly one 𝑦"), analogous to 2eu4 2555 with the additional requirement that the restricting classes are not empty (which is not necessary as shown in 2reu4 40515). (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 3382 . . . 4 (∃!𝑥𝐴𝑦𝐵 𝜑 ↔ (∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧)))
2 reu3 3382 . . . 4 (∃!𝑦𝐵𝑥𝐴 𝜑 ↔ (∃𝑦𝐵𝑥𝐴 𝜑 ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤)))
31, 2anbi12i 732 . . 3 ((∃!𝑥𝐴𝑦𝐵 𝜑 ∧ ∃!𝑦𝐵𝑥𝐴 𝜑) ↔ ((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧)) ∧ (∃𝑦𝐵𝑥𝐴 𝜑 ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))))
43a1i 11 . 2 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃!𝑥𝐴𝑦𝐵 𝜑 ∧ ∃!𝑦𝐵𝑥𝐴 𝜑) ↔ ((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧)) ∧ (∃𝑦𝐵𝑥𝐴 𝜑 ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤)))))
5 an4 864 . . 3 (((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧)) ∧ (∃𝑦𝐵𝑥𝐴 𝜑 ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))) ↔ ((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑦𝐵𝑥𝐴 𝜑) ∧ (∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))))
65a1i 11 . 2 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧)) ∧ (∃𝑦𝐵𝑥𝐴 𝜑 ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))) ↔ ((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑦𝐵𝑥𝐴 𝜑) ∧ (∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤)))))
7 rexcom 3092 . . . . . 6 (∃𝑦𝐵𝑥𝐴 𝜑 ↔ ∃𝑥𝐴𝑦𝐵 𝜑)
87anbi2i 729 . . . . 5 ((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑦𝐵𝑥𝐴 𝜑) ↔ (∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑥𝐴𝑦𝐵 𝜑))
9 anidm 675 . . . . 5 ((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑥𝐴𝑦𝐵 𝜑) ↔ ∃𝑥𝐴𝑦𝐵 𝜑)
108, 9bitri 264 . . . 4 ((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑦𝐵𝑥𝐴 𝜑) ↔ ∃𝑥𝐴𝑦𝐵 𝜑)
1110a1i 11 . . 3 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑦𝐵𝑥𝐴 𝜑) ↔ ∃𝑥𝐴𝑦𝐵 𝜑))
12 r19.26 3058 . . . . . . . 8 (∀𝑥𝐴 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)) ↔ (∀𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)))
13 nfra1 2936 . . . . . . . . . . . . . 14 𝑥𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)
1413r19.3rz 4039 . . . . . . . . . . . . 13 (𝐴 ≠ ∅ → (∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤) ↔ ∀𝑥𝐴𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)))
1514bicomd 213 . . . . . . . . . . . 12 (𝐴 ≠ ∅ → (∀𝑥𝐴𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤) ↔ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)))
1615adantr 481 . . . . . . . . . . 11 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (∀𝑥𝐴𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤) ↔ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)))
1716adantr 481 . . . . . . . . . 10 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑥𝐴𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤) ↔ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)))
1817anbi2d 739 . . . . . . . . 9 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → ((∀𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)) ↔ (∀𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤))))
19 jcab 906 . . . . . . . . . . . . . 14 ((𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ ((𝜑𝑥 = 𝑧) ∧ (𝜑𝑦 = 𝑤)))
2019ralbii 2975 . . . . . . . . . . . . 13 (∀𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ ∀𝑦𝐵 ((𝜑𝑥 = 𝑧) ∧ (𝜑𝑦 = 𝑤)))
21 r19.26 3058 . . . . . . . . . . . . 13 (∀𝑦𝐵 ((𝜑𝑥 = 𝑧) ∧ (𝜑𝑦 = 𝑤)) ↔ (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (𝜑𝑦 = 𝑤)))
2220, 21bitri 264 . . . . . . . . . . . 12 (∀𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (𝜑𝑦 = 𝑤)))
2322ralbii 2975 . . . . . . . . . . 11 (∀𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ ∀𝑥𝐴 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (𝜑𝑦 = 𝑤)))
24 r19.26 3058 . . . . . . . . . . 11 (∀𝑥𝐴 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (𝜑𝑦 = 𝑤)) ↔ (∀𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)))
2523, 24bitri 264 . . . . . . . . . 10 (∀𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ (∀𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)))
2625a1i 11 . . . . . . . . 9 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ (∀𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤))))
2718, 26bitr4d 271 . . . . . . . 8 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → ((∀𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)) ↔ ∀𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤))))
2812, 27syl5rbb 273 . . . . . . 7 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ ∀𝑥𝐴 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤))))
29 r19.26 3058 . . . . . . . . 9 (∀𝑦𝐵 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴 (𝜑𝑦 = 𝑤)) ↔ (∀𝑦𝐵𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵𝑥𝐴 (𝜑𝑦 = 𝑤)))
30 nfra1 2936 . . . . . . . . . . . . 13 𝑦𝑦𝐵 (𝜑𝑥 = 𝑧)
3130r19.3rz 4039 . . . . . . . . . . . 12 (𝐵 ≠ ∅ → (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ↔ ∀𝑦𝐵𝑦𝐵 (𝜑𝑥 = 𝑧)))
3231ad2antlr 762 . . . . . . . . . . 11 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ↔ ∀𝑦𝐵𝑦𝐵 (𝜑𝑥 = 𝑧)))
3332bicomd 213 . . . . . . . . . 10 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑦𝐵𝑦𝐵 (𝜑𝑥 = 𝑧) ↔ ∀𝑦𝐵 (𝜑𝑥 = 𝑧)))
34 ralcom 3091 . . . . . . . . . . 11 (∀𝑦𝐵𝑥𝐴 (𝜑𝑦 = 𝑤) ↔ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤))
3534a1i 11 . . . . . . . . . 10 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑦𝐵𝑥𝐴 (𝜑𝑦 = 𝑤) ↔ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)))
3633, 35anbi12d 746 . . . . . . . . 9 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → ((∀𝑦𝐵𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵𝑥𝐴 (𝜑𝑦 = 𝑤)) ↔ (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤))))
3729, 36syl5bb 272 . . . . . . . 8 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑦𝐵 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴 (𝜑𝑦 = 𝑤)) ↔ (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤))))
3837ralbidv 2981 . . . . . . 7 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑥𝐴𝑦𝐵 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴 (𝜑𝑦 = 𝑤)) ↔ ∀𝑥𝐴 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤))))
3928, 38bitr4d 271 . . . . . 6 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ ∀𝑥𝐴𝑦𝐵 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴 (𝜑𝑦 = 𝑤))))
40 r19.23v 3017 . . . . . . . . 9 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ↔ (∃𝑦𝐵 𝜑𝑥 = 𝑧))
41 r19.23v 3017 . . . . . . . . 9 (∀𝑥𝐴 (𝜑𝑦 = 𝑤) ↔ (∃𝑥𝐴 𝜑𝑦 = 𝑤))
4240, 41anbi12i 732 . . . . . . . 8 ((∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴 (𝜑𝑦 = 𝑤)) ↔ ((∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ (∃𝑥𝐴 𝜑𝑦 = 𝑤)))
43422ralbii 2976 . . . . . . 7 (∀𝑥𝐴𝑦𝐵 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴 (𝜑𝑦 = 𝑤)) ↔ ∀𝑥𝐴𝑦𝐵 ((∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ (∃𝑥𝐴 𝜑𝑦 = 𝑤)))
4443a1i 11 . . . . . 6 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑥𝐴𝑦𝐵 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴 (𝜑𝑦 = 𝑤)) ↔ ∀𝑥𝐴𝑦𝐵 ((∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ (∃𝑥𝐴 𝜑𝑦 = 𝑤))))
45 neneq 2796 . . . . . . . . . . 11 (𝐴 ≠ ∅ → ¬ 𝐴 = ∅)
46 neneq 2796 . . . . . . . . . . 11 (𝐵 ≠ ∅ → ¬ 𝐵 = ∅)
4745, 46anim12i 589 . . . . . . . . . 10 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅))
4847olcd 408 . . . . . . . . 9 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅)))
49 dfbi3 993 . . . . . . . . 9 ((𝐴 = ∅ ↔ 𝐵 = ∅) ↔ ((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅)))
5048, 49sylibr 224 . . . . . . . 8 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (𝐴 = ∅ ↔ 𝐵 = ∅))
51 nfre1 3000 . . . . . . . . . 10 𝑦𝑦𝐵 𝜑
52 nfv 1840 . . . . . . . . . 10 𝑦 𝑥 = 𝑧
5351, 52nfim 1822 . . . . . . . . 9 𝑦(∃𝑦𝐵 𝜑𝑥 = 𝑧)
54 nfre1 3000 . . . . . . . . . 10 𝑥𝑥𝐴 𝜑
55 nfv 1840 . . . . . . . . . 10 𝑥 𝑦 = 𝑤
5654, 55nfim 1822 . . . . . . . . 9 𝑥(∃𝑥𝐴 𝜑𝑦 = 𝑤)
5753, 56raaan2 40500 . . . . . . . 8 ((𝐴 = ∅ ↔ 𝐵 = ∅) → (∀𝑥𝐴𝑦𝐵 ((∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ (∃𝑥𝐴 𝜑𝑦 = 𝑤)) ↔ (∀𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))))
5850, 57syl 17 . . . . . . 7 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (∀𝑥𝐴𝑦𝐵 ((∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ (∃𝑥𝐴 𝜑𝑦 = 𝑤)) ↔ (∀𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))))
5958adantr 481 . . . . . 6 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑥𝐴𝑦𝐵 ((∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ (∃𝑥𝐴 𝜑𝑦 = 𝑤)) ↔ (∀𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))))
6039, 44, 593bitrd 294 . . . . 5 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ (∀𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))))
61602rexbidva 3050 . . . 4 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (∃𝑧𝐴𝑤𝐵𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ ∃𝑧𝐴𝑤𝐵 (∀𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))))
62 reeanv 3100 . . . 4 (∃𝑧𝐴𝑤𝐵 (∀𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤)) ↔ (∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤)))
6361, 62syl6rbb 277 . . 3 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤)) ↔ ∃𝑧𝐴𝑤𝐵𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤))))
6411, 63anbi12d 746 . 2 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑦𝐵𝑥𝐴 𝜑) ∧ (∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))) ↔ (∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑧𝐴𝑤𝐵𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)))))
654, 6, 643bitrd 294 1 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃!𝑥𝐴𝑦𝐵 𝜑 ∧ ∃!𝑦𝐵𝑥𝐴 𝜑) ↔ (∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑧𝐴𝑤𝐵𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384   = wceq 1480  wcel 1987  wne 2790  wral 2907  wrex 2908  ∃!wreu 2909  c0 3896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-v 3191  df-dif 3562  df-nul 3897
This theorem is referenced by:  2reu4  40515
  Copyright terms: Public domain W3C validator