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 41886
Description: Definition of double restricted existential uniqueness ("exactly one 𝑥 and exactly one 𝑦"), analogous to 2eu4 2678 with the additional requirement that the restricting classes are not empty (which is not necessary as shown in 2reu4 41887). (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 3557 . . . 4 (∃!𝑥𝐴𝑦𝐵 𝜑 ↔ (∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧)))
2 reu3 3557 . . . 4 (∃!𝑦𝐵𝑥𝐴 𝜑 ↔ (∃𝑦𝐵𝑥𝐴 𝜑 ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤)))
31, 2anbi12i 620 . . 3 ((∃!𝑥𝐴𝑦𝐵 𝜑 ∧ ∃!𝑦𝐵𝑥𝐴 𝜑) ↔ ((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧)) ∧ (∃𝑦𝐵𝑥𝐴 𝜑 ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))))
43a1i 11 . 2 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃!𝑥𝐴𝑦𝐵 𝜑 ∧ ∃!𝑦𝐵𝑥𝐴 𝜑) ↔ ((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧)) ∧ (∃𝑦𝐵𝑥𝐴 𝜑 ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤)))))
5 an4 646 . . 3 (((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧)) ∧ (∃𝑦𝐵𝑥𝐴 𝜑 ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))) ↔ ((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑦𝐵𝑥𝐴 𝜑) ∧ (∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))))
65a1i 11 . 2 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧)) ∧ (∃𝑦𝐵𝑥𝐴 𝜑 ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))) ↔ ((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑦𝐵𝑥𝐴 𝜑) ∧ (∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤)))))
7 rexcom 3246 . . . . . 6 (∃𝑦𝐵𝑥𝐴 𝜑 ↔ ∃𝑥𝐴𝑦𝐵 𝜑)
87anbi2i 616 . . . . 5 ((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑦𝐵𝑥𝐴 𝜑) ↔ (∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑥𝐴𝑦𝐵 𝜑))
9 anidm 560 . . . . 5 ((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑥𝐴𝑦𝐵 𝜑) ↔ ∃𝑥𝐴𝑦𝐵 𝜑)
108, 9bitri 266 . . . 4 ((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑦𝐵𝑥𝐴 𝜑) ↔ ∃𝑥𝐴𝑦𝐵 𝜑)
1110a1i 11 . . 3 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑦𝐵𝑥𝐴 𝜑) ↔ ∃𝑥𝐴𝑦𝐵 𝜑))
12 r19.26 3211 . . . . . . . 8 (∀𝑥𝐴 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)) ↔ (∀𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)))
13 nfra1 3088 . . . . . . . . . . . . . 14 𝑥𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)
1413r19.3rz 4223 . . . . . . . . . . . . 13 (𝐴 ≠ ∅ → (∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤) ↔ ∀𝑥𝐴𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)))
1514bicomd 214 . . . . . . . . . . . 12 (𝐴 ≠ ∅ → (∀𝑥𝐴𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤) ↔ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)))
1615adantr 472 . . . . . . . . . . 11 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (∀𝑥𝐴𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤) ↔ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)))
1716adantr 472 . . . . . . . . . 10 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑥𝐴𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤) ↔ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)))
1817anbi2d 622 . . . . . . . . 9 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → ((∀𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)) ↔ (∀𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤))))
19 jcab 513 . . . . . . . . . . . . . 14 ((𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ ((𝜑𝑥 = 𝑧) ∧ (𝜑𝑦 = 𝑤)))
2019ralbii 3127 . . . . . . . . . . . . 13 (∀𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ ∀𝑦𝐵 ((𝜑𝑥 = 𝑧) ∧ (𝜑𝑦 = 𝑤)))
21 r19.26 3211 . . . . . . . . . . . . 13 (∀𝑦𝐵 ((𝜑𝑥 = 𝑧) ∧ (𝜑𝑦 = 𝑤)) ↔ (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (𝜑𝑦 = 𝑤)))
2220, 21bitri 266 . . . . . . . . . . . 12 (∀𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (𝜑𝑦 = 𝑤)))
2322ralbii 3127 . . . . . . . . . . 11 (∀𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ ∀𝑥𝐴 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (𝜑𝑦 = 𝑤)))
24 r19.26 3211 . . . . . . . . . . 11 (∀𝑥𝐴 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (𝜑𝑦 = 𝑤)) ↔ (∀𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)))
2523, 24bitri 266 . . . . . . . . . 10 (∀𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ (∀𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)))
2625a1i 11 . . . . . . . . 9 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ (∀𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤))))
2718, 26bitr4d 273 . . . . . . . 8 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → ((∀𝑥𝐴𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)) ↔ ∀𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤))))
2812, 27syl5rbb 275 . . . . . . 7 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ ∀𝑥𝐴 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤))))
29 r19.26 3211 . . . . . . . . 9 (∀𝑦𝐵 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴 (𝜑𝑦 = 𝑤)) ↔ (∀𝑦𝐵𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵𝑥𝐴 (𝜑𝑦 = 𝑤)))
30 nfra1 3088 . . . . . . . . . . . . 13 𝑦𝑦𝐵 (𝜑𝑥 = 𝑧)
3130r19.3rz 4223 . . . . . . . . . . . 12 (𝐵 ≠ ∅ → (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ↔ ∀𝑦𝐵𝑦𝐵 (𝜑𝑥 = 𝑧)))
3231ad2antlr 718 . . . . . . . . . . 11 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ↔ ∀𝑦𝐵𝑦𝐵 (𝜑𝑥 = 𝑧)))
3332bicomd 214 . . . . . . . . . 10 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑦𝐵𝑦𝐵 (𝜑𝑥 = 𝑧) ↔ ∀𝑦𝐵 (𝜑𝑥 = 𝑧)))
34 ralcom 3245 . . . . . . . . . . 11 (∀𝑦𝐵𝑥𝐴 (𝜑𝑦 = 𝑤) ↔ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤))
3534a1i 11 . . . . . . . . . 10 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑦𝐵𝑥𝐴 (𝜑𝑦 = 𝑤) ↔ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤)))
3633, 35anbi12d 624 . . . . . . . . 9 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → ((∀𝑦𝐵𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵𝑥𝐴 (𝜑𝑦 = 𝑤)) ↔ (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤))))
3729, 36syl5bb 274 . . . . . . . 8 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑦𝐵 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴 (𝜑𝑦 = 𝑤)) ↔ (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤))))
3837ralbidv 3133 . . . . . . 7 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑥𝐴𝑦𝐵 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴 (𝜑𝑦 = 𝑤)) ↔ ∀𝑥𝐴 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴𝑦𝐵 (𝜑𝑦 = 𝑤))))
3928, 38bitr4d 273 . . . . . 6 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ ∀𝑥𝐴𝑦𝐵 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴 (𝜑𝑦 = 𝑤))))
40 r19.23v 3170 . . . . . . . . 9 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ↔ (∃𝑦𝐵 𝜑𝑥 = 𝑧))
41 r19.23v 3170 . . . . . . . . 9 (∀𝑥𝐴 (𝜑𝑦 = 𝑤) ↔ (∃𝑥𝐴 𝜑𝑦 = 𝑤))
4240, 41anbi12i 620 . . . . . . . 8 ((∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴 (𝜑𝑦 = 𝑤)) ↔ ((∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ (∃𝑥𝐴 𝜑𝑦 = 𝑤)))
43422ralbii 3128 . . . . . . 7 (∀𝑥𝐴𝑦𝐵 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴 (𝜑𝑦 = 𝑤)) ↔ ∀𝑥𝐴𝑦𝐵 ((∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ (∃𝑥𝐴 𝜑𝑦 = 𝑤)))
4443a1i 11 . . . . . 6 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑥𝐴𝑦𝐵 (∀𝑦𝐵 (𝜑𝑥 = 𝑧) ∧ ∀𝑥𝐴 (𝜑𝑦 = 𝑤)) ↔ ∀𝑥𝐴𝑦𝐵 ((∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ (∃𝑥𝐴 𝜑𝑦 = 𝑤))))
45 neneq 2943 . . . . . . . . . . 11 (𝐴 ≠ ∅ → ¬ 𝐴 = ∅)
46 neneq 2943 . . . . . . . . . . 11 (𝐵 ≠ ∅ → ¬ 𝐵 = ∅)
4745, 46anim12i 606 . . . . . . . . . 10 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅))
4847olcd 900 . . . . . . . . 9 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅)))
49 dfbi3 1072 . . . . . . . . 9 ((𝐴 = ∅ ↔ 𝐵 = ∅) ↔ ((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅)))
5048, 49sylibr 225 . . . . . . . 8 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (𝐴 = ∅ ↔ 𝐵 = ∅))
51 nfre1 3151 . . . . . . . . . 10 𝑦𝑦𝐵 𝜑
52 nfv 2009 . . . . . . . . . 10 𝑦 𝑥 = 𝑧
5351, 52nfim 1995 . . . . . . . . 9 𝑦(∃𝑦𝐵 𝜑𝑥 = 𝑧)
54 nfre1 3151 . . . . . . . . . 10 𝑥𝑥𝐴 𝜑
55 nfv 2009 . . . . . . . . . 10 𝑥 𝑦 = 𝑤
5654, 55nfim 1995 . . . . . . . . 9 𝑥(∃𝑥𝐴 𝜑𝑦 = 𝑤)
5753, 56raaan2 41833 . . . . . . . 8 ((𝐴 = ∅ ↔ 𝐵 = ∅) → (∀𝑥𝐴𝑦𝐵 ((∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ (∃𝑥𝐴 𝜑𝑦 = 𝑤)) ↔ (∀𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))))
5850, 57syl 17 . . . . . . 7 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (∀𝑥𝐴𝑦𝐵 ((∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ (∃𝑥𝐴 𝜑𝑦 = 𝑤)) ↔ (∀𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))))
5958adantr 472 . . . . . 6 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑥𝐴𝑦𝐵 ((∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ (∃𝑥𝐴 𝜑𝑦 = 𝑤)) ↔ (∀𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))))
6039, 44, 593bitrd 296 . . . . 5 (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ (𝑧𝐴𝑤𝐵)) → (∀𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ (∀𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))))
61602rexbidva 3203 . . . 4 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (∃𝑧𝐴𝑤𝐵𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)) ↔ ∃𝑧𝐴𝑤𝐵 (∀𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))))
62 reeanv 3254 . . . 4 (∃𝑧𝐴𝑤𝐵 (∀𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∀𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤)) ↔ (∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤)))
6361, 62syl6rbb 279 . . 3 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤)) ↔ ∃𝑧𝐴𝑤𝐵𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤))))
6411, 63anbi12d 624 . 2 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (((∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑦𝐵𝑥𝐴 𝜑) ∧ (∃𝑧𝐴𝑥𝐴 (∃𝑦𝐵 𝜑𝑥 = 𝑧) ∧ ∃𝑤𝐵𝑦𝐵 (∃𝑥𝐴 𝜑𝑦 = 𝑤))) ↔ (∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑧𝐴𝑤𝐵𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)))))
654, 6, 643bitrd 296 1 ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((∃!𝑥𝐴𝑦𝐵 𝜑 ∧ ∃!𝑦𝐵𝑥𝐴 𝜑) ↔ (∃𝑥𝐴𝑦𝐵 𝜑 ∧ ∃𝑧𝐴𝑤𝐵𝑥𝐴𝑦𝐵 (𝜑 → (𝑥 = 𝑧𝑦 = 𝑤)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 873   = wceq 1652  wcel 2155  wne 2937  wral 3055  wrex 3056  ∃!wreu 3057  c0 4081
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-v 3352  df-dif 3737  df-nul 4082
This theorem is referenced by:  2reu4  41887
  Copyright terms: Public domain W3C validator