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 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
StepHypRef Expression
1 reu3 3363 . . . 4 (∃!𝑥𝐴𝑦𝐵 𝜑 ↔ (∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧)))
2 reu3 3363 . . . 4 (∃!𝑦𝐵𝑥𝐴 𝜑 ↔ (∃𝑦𝐵𝑥𝐴 𝜑 ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤)))
31, 2anbi12i 729 . . 3 ((∃!𝑥𝐴𝑦𝐵 𝜑 ∧ ∃!𝑦𝐵𝑥𝐴 𝜑) ↔ ((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧)) ∧ (∃𝑦𝐵𝑥𝐴 𝜑 ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))))
43a1i 11 . 2 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃!𝑥𝐴𝑦𝐵 𝜑 ∧ ∃!𝑦𝐵𝑥𝐴 𝜑) ↔ ((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧)) ∧ (∃𝑦𝐵𝑥𝐴 𝜑 ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤)))))
5 an4 861 . . 3 (((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧)) ∧ (∃𝑦𝐵𝑥𝐴 𝜑 ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))) ↔ ((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑦𝐵𝑥𝐴 𝜑) ∧ (∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))))
65a1i 11 . 2 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧)) ∧ (∃𝑦𝐵𝑥𝐴 𝜑 ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))) ↔ ((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑦𝐵𝑥𝐴 𝜑) ∧ (∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤)))))
7 rexcom 3080 . . . . . 6 (∃𝑦𝐵𝑥𝐴 𝜑 ↔ ∃𝑥𝐴𝑦𝐵 𝜑)
87anbi2i 726 . . . . 5 ((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑦𝐵𝑥𝐴 𝜑) ↔ (∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑥𝐴𝑦𝐵 𝜑))
9 anidm 674 . . . . 5 ((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑥𝐴𝑦𝐵 𝜑) ↔ ∃𝑥𝐴𝑦𝐵 𝜑)
108, 9bitri 263 . . . 4 ((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑦𝐵𝑥𝐴 𝜑) ↔ ∃𝑥𝐴𝑦𝐵 𝜑)
1110a1i 11 . . 3 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑦𝐵𝑥𝐴 𝜑) ↔ ∃𝑥𝐴𝑦𝐵 𝜑))
12 r19.26 3046 . . . . . . . 8 (∀𝑥𝐴 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)) ↔ (∀𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)))
13 nfra1 2925 . . . . . . . . . . . . . 14 𝑥𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)
1413r19.3rz 4014 . . . . . . . . . . . . 13 (𝐴 ≠ ∅ → (∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤) ↔ ∀𝑥𝐴𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)))
1514bicomd 212 . . . . . . . . . . . 12 (𝐴 ≠ ∅ → (∀𝑥𝐴𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤) ↔ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)))
1615adantr 480 . . . . . . . . . . 11 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (∀𝑥𝐴𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤) ↔ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)))
1716adantr 480 . . . . . . . . . 10 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑥𝐴𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤) ↔ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)))
1817anbi2d 736 . . . . . . . . 9 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → ((∀𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)) ↔ (∀𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤))))
19 jcab 903 . . . . . . . . . . . . . 14 ((𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ ((𝜑𝑥 = 𝑧) ∧ (𝜑𝑦 = 𝑤)))
2019ralbii 2963 . . . . . . . . . . . . 13 (∀𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ ∀𝑦𝐵 ((𝜑𝑥 = 𝑧) ∧ (𝜑𝑦 = 𝑤)))
21 r19.26 3046 . . . . . . . . . . . . 13 (∀𝑦𝐵 ((𝜑𝑥 = 𝑧) ∧ (𝜑𝑦 = 𝑤)) ↔ (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (𝜑𝑦 = 𝑤)))
2220, 21bitri 263 . . . . . . . . . . . 12 (∀𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (𝜑𝑦 = 𝑤)))
2322ralbii 2963 . . . . . . . . . . 11 (∀𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ ∀𝑥𝐴 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (𝜑𝑦 = 𝑤)))
24 r19.26 3046 . . . . . . . . . . 11 (∀𝑥𝐴 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (𝜑𝑦 = 𝑤)) ↔ (∀𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)))
2523, 24bitri 263 . . . . . . . . . 10 (∀𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ (∀𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)))
2625a1i 11 . . . . . . . . 9 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ (∀𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤))))
2718, 26bitr4d 270 . . . . . . . 8 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → ((∀𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)) ↔ ∀𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤))))
2812, 27syl5rbb 272 . . . . . . 7 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ ∀𝑥𝐴 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤))))
29 r19.26 3046 . . . . . . . . 9 (∀𝑦𝐵 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴 (𝜑𝑦 = 𝑤)) ↔ (∀𝑦𝐵𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵𝑥𝐴 (𝜑𝑦 = 𝑤)))
30 nfra1 2925 . . . . . . . . . . . . 13 𝑦𝑦𝐵 (𝜑𝑥 = 𝑧)
3130r19.3rz 4014 . . . . . . . . . . . 12 (𝐵 ≠ ∅ → (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ↔ ∀𝑦𝐵𝑦𝐵 (𝜑𝑥 = 𝑧)))
3231ad2antlr 759 . . . . . . . . . . 11 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ↔ ∀𝑦𝐵𝑦𝐵 (𝜑𝑥 = 𝑧)))
3332bicomd 212 . . . . . . . . . 10 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑦𝐵𝑦𝐵 (𝜑𝑥 = 𝑧) ↔ ∀𝑦𝐵 (𝜑𝑥 = 𝑧)))
34 ralcom 3079 . . . . . . . . . . 11 (∀𝑦𝐵𝑥𝐴 (𝜑𝑦 = 𝑤) ↔ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤))
3534a1i 11 . . . . . . . . . 10 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑦𝐵𝑥𝐴 (𝜑𝑦 = 𝑤) ↔ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)))
3633, 35anbi12d 743 . . . . . . . . 9 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → ((∀𝑦𝐵𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵𝑥𝐴 (𝜑𝑦 = 𝑤)) ↔ (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤))))
3729, 36syl5bb 271 . . . . . . . 8 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑦𝐵 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴 (𝜑𝑦 = 𝑤)) ↔ (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤))))
3837ralbidv 2969 . . . . . . 7 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑥𝐴𝑦𝐵 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴 (𝜑𝑦 = 𝑤)) ↔ ∀𝑥𝐴 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤))))
3928, 38bitr4d 270 . . . . . 6 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ ∀𝑥𝐴𝑦𝐵 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴 (𝜑𝑦 = 𝑤))))
40 r19.23v 3005 . . . . . . . . 9 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ↔ (∃𝑦𝐵 𝜑𝑥 = 𝑧))
41 r19.23v 3005 . . . . . . . . 9 (∀𝑥𝐴 (𝜑𝑦 = 𝑤) ↔ (∃𝑥𝐴 𝜑𝑦 = 𝑤))
4240, 41anbi12i 729 . . . . . . . 8 ((∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴 (𝜑𝑦 = 𝑤)) ↔ ((∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ (∃𝑥𝐴 𝜑𝑦 = 𝑤)))
43422ralbii 2964 . . . . . . 7 (∀𝑥𝐴𝑦𝐵 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴 (𝜑𝑦 = 𝑤)) ↔ ∀𝑥𝐴𝑦𝐵 ((∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ (∃𝑥𝐴 𝜑𝑦 = 𝑤)))
4443a1i 11 . . . . . 6 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑥𝐴𝑦𝐵 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴 (𝜑𝑦 = 𝑤)) ↔ ∀𝑥𝐴𝑦𝐵 ((∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ (∃𝑥𝐴 𝜑𝑦 = 𝑤))))
45 df-ne 2782 . . . . . . . . . . . 12 (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅)
4645biimpi 205 . . . . . . . . . . 11 (𝐴 ≠ ∅ → ¬ 𝐴 = ∅)
47 df-ne 2782 . . . . . . . . . . . 12 (𝐵 ≠ ∅ ↔ ¬ 𝐵 = ∅)
4847biimpi 205 . . . . . . . . . . 11 (𝐵 ≠ ∅ → ¬ 𝐵 = ∅)
4946, 48anim12i 588 . . . . . . . . . 10 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅))
5049olcd 407 . . . . . . . . 9 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅)))
51 dfbi3 933 . . . . . . . . 9 ((𝐴 = ∅ ↔ 𝐵 = ∅) ↔ ((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅)))
5250, 51sylibr 223 . . . . . . . 8 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (𝐴 = ∅ ↔ 𝐵 = ∅))
53 nfre1 2988 . . . . . . . . . 10 𝑦𝑦𝐵 𝜑
54 nfv 1830 . . . . . . . . . 10 𝑦 𝑥 = 𝑧
5553, 54nfim 1813 . . . . . . . . 9 𝑦(∃𝑦𝐵 𝜑𝑥 = 𝑧)
56 nfre1 2988 . . . . . . . . . 10 𝑥𝑥𝐴 𝜑
57 nfv 1830 . . . . . . . . . 10 𝑥 𝑦 = 𝑤
5856, 57nfim 1813 . . . . . . . . 9 𝑥(∃𝑥𝐴 𝜑𝑦 = 𝑤)
5955, 58raaan2 39824 . . . . . . . 8 ((𝐴 = ∅ ↔ 𝐵 = ∅) → (∀𝑥𝐴𝑦𝐵 ((∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ (∃𝑥𝐴 𝜑𝑦 = 𝑤)) ↔ (∀𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))))
6052, 59syl 17 . . . . . . 7 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (∀𝑥𝐴𝑦𝐵 ((∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ (∃𝑥𝐴 𝜑𝑦 = 𝑤)) ↔ (∀𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))))
6160adantr 480 . . . . . 6 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑥𝐴𝑦𝐵 ((∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ (∃𝑥𝐴 𝜑𝑦 = 𝑤)) ↔ (∀𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))))
6239, 44, 613bitrd 293 . . . . 5 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ (∀𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))))
63622rexbidva 3038 . . . 4 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (∃𝑧𝐴𝑤𝐵𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ ∃𝑧𝐴𝑤𝐵 (∀𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))))
64 reeanv 3086 . . . 4 (∃𝑧𝐴𝑤𝐵 (∀𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤)) ↔ (∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤)))
6563, 64syl6rbb 276 . . 3 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤)) ↔ ∃𝑧𝐴𝑤𝐵𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤))))
6611, 65anbi12d 743 . 2 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑦𝐵𝑥𝐴 𝜑) ∧ (∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))) ↔ (∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑧𝐴𝑤𝐵𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)))))
674, 6, 663bitrd 293 1 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃!𝑥𝐴𝑦𝐵 𝜑 ∧ ∃!𝑦𝐵𝑥𝐴 𝜑) ↔ (∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑧𝐴𝑤𝐵𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)))))
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator