Metamath Proof Explorer


Theorem 2reu4lem

Description: Lemma for 2reu4 . (Contributed by Alexander van der Vekens, 1-Jul-2017)

Ref Expression
Assertion 2reu4lem ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) → ( ( ∃! 𝑥𝐴𝑦𝐵 𝜑 ∧ ∃! 𝑦𝐵𝑥𝐴 𝜑 ) ↔ ( ∃ 𝑥𝐴𝑦𝐵 𝜑 ∧ ∃ 𝑧𝐴𝑤𝐵𝑥𝐴𝑦𝐵 ( 𝜑 → ( 𝑥 = 𝑧𝑦 = 𝑤 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 reu3 ( ∃! 𝑥𝐴𝑦𝐵 𝜑 ↔ ( ∃ 𝑥𝐴𝑦𝐵 𝜑 ∧ ∃ 𝑧𝐴𝑥𝐴 ( ∃ 𝑦𝐵 𝜑𝑥 = 𝑧 ) ) )
2 reu3 ( ∃! 𝑦𝐵𝑥𝐴 𝜑 ↔ ( ∃ 𝑦𝐵𝑥𝐴 𝜑 ∧ ∃ 𝑤𝐵𝑦𝐵 ( ∃ 𝑥𝐴 𝜑𝑦 = 𝑤 ) ) )
3 1 2 anbi12i ( ( ∃! 𝑥𝐴𝑦𝐵 𝜑 ∧ ∃! 𝑦𝐵𝑥𝐴 𝜑 ) ↔ ( ( ∃ 𝑥𝐴𝑦𝐵 𝜑 ∧ ∃ 𝑧𝐴𝑥𝐴 ( ∃ 𝑦𝐵 𝜑𝑥 = 𝑧 ) ) ∧ ( ∃ 𝑦𝐵𝑥𝐴 𝜑 ∧ ∃ 𝑤𝐵𝑦𝐵 ( ∃ 𝑥𝐴 𝜑𝑦 = 𝑤 ) ) ) )
4 3 a1i ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) → ( ( ∃! 𝑥𝐴𝑦𝐵 𝜑 ∧ ∃! 𝑦𝐵𝑥𝐴 𝜑 ) ↔ ( ( ∃ 𝑥𝐴𝑦𝐵 𝜑 ∧ ∃ 𝑧𝐴𝑥𝐴 ( ∃ 𝑦𝐵 𝜑𝑥 = 𝑧 ) ) ∧ ( ∃ 𝑦𝐵𝑥𝐴 𝜑 ∧ ∃ 𝑤𝐵𝑦𝐵 ( ∃ 𝑥𝐴 𝜑𝑦 = 𝑤 ) ) ) ) )
5 an4 ( ( ( ∃ 𝑥𝐴𝑦𝐵 𝜑 ∧ ∃ 𝑧𝐴𝑥𝐴 ( ∃ 𝑦𝐵 𝜑𝑥 = 𝑧 ) ) ∧ ( ∃ 𝑦𝐵𝑥𝐴 𝜑 ∧ ∃ 𝑤𝐵𝑦𝐵 ( ∃ 𝑥𝐴 𝜑𝑦 = 𝑤 ) ) ) ↔ ( ( ∃ 𝑥𝐴𝑦𝐵 𝜑 ∧ ∃ 𝑦𝐵𝑥𝐴 𝜑 ) ∧ ( ∃ 𝑧𝐴𝑥𝐴 ( ∃ 𝑦𝐵 𝜑𝑥 = 𝑧 ) ∧ ∃ 𝑤𝐵𝑦𝐵 ( ∃ 𝑥𝐴 𝜑𝑦 = 𝑤 ) ) ) )
6 5 a1i ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) → ( ( ( ∃ 𝑥𝐴𝑦𝐵 𝜑 ∧ ∃ 𝑧𝐴𝑥𝐴 ( ∃ 𝑦𝐵 𝜑𝑥 = 𝑧 ) ) ∧ ( ∃ 𝑦𝐵𝑥𝐴 𝜑 ∧ ∃ 𝑤𝐵𝑦𝐵 ( ∃ 𝑥𝐴 𝜑𝑦 = 𝑤 ) ) ) ↔ ( ( ∃ 𝑥𝐴𝑦𝐵 𝜑 ∧ ∃ 𝑦𝐵𝑥𝐴 𝜑 ) ∧ ( ∃ 𝑧𝐴𝑥𝐴 ( ∃ 𝑦𝐵 𝜑𝑥 = 𝑧 ) ∧ ∃ 𝑤𝐵𝑦𝐵 ( ∃ 𝑥𝐴 𝜑𝑦 = 𝑤 ) ) ) ) )
7 rexcom ( ∃ 𝑦𝐵𝑥𝐴 𝜑 ↔ ∃ 𝑥𝐴𝑦𝐵 𝜑 )
8 7 anbi2i ( ( ∃ 𝑥𝐴𝑦𝐵 𝜑 ∧ ∃ 𝑦𝐵𝑥𝐴 𝜑 ) ↔ ( ∃ 𝑥𝐴𝑦𝐵 𝜑 ∧ ∃ 𝑥𝐴𝑦𝐵 𝜑 ) )
9 anidm ( ( ∃ 𝑥𝐴𝑦𝐵 𝜑 ∧ ∃ 𝑥𝐴𝑦𝐵 𝜑 ) ↔ ∃ 𝑥𝐴𝑦𝐵 𝜑 )
10 8 9 bitri ( ( ∃ 𝑥𝐴𝑦𝐵 𝜑 ∧ ∃ 𝑦𝐵𝑥𝐴 𝜑 ) ↔ ∃ 𝑥𝐴𝑦𝐵 𝜑 )
11 10 a1i ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) → ( ( ∃ 𝑥𝐴𝑦𝐵 𝜑 ∧ ∃ 𝑦𝐵𝑥𝐴 𝜑 ) ↔ ∃ 𝑥𝐴𝑦𝐵 𝜑 ) )
12 r19.26 ( ∀ 𝑥𝐴 ( ∀ 𝑦𝐵 ( 𝜑𝑥 = 𝑧 ) ∧ ∀ 𝑥𝐴𝑦𝐵 ( 𝜑𝑦 = 𝑤 ) ) ↔ ( ∀ 𝑥𝐴𝑦𝐵 ( 𝜑𝑥 = 𝑧 ) ∧ ∀ 𝑥𝐴𝑥𝐴𝑦𝐵 ( 𝜑𝑦 = 𝑤 ) ) )
13 nfra1 𝑥𝑥𝐴𝑦𝐵 ( 𝜑𝑦 = 𝑤 )
14 13 r19.3rz ( 𝐴 ≠ ∅ → ( ∀ 𝑥𝐴𝑦𝐵 ( 𝜑𝑦 = 𝑤 ) ↔ ∀ 𝑥𝐴𝑥𝐴𝑦𝐵 ( 𝜑𝑦 = 𝑤 ) ) )
15 14 bicomd ( 𝐴 ≠ ∅ → ( ∀ 𝑥𝐴𝑥𝐴𝑦𝐵 ( 𝜑𝑦 = 𝑤 ) ↔ ∀ 𝑥𝐴𝑦𝐵 ( 𝜑𝑦 = 𝑤 ) ) )
16 15 adantr ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) → ( ∀ 𝑥𝐴𝑥𝐴𝑦𝐵 ( 𝜑𝑦 = 𝑤 ) ↔ ∀ 𝑥𝐴𝑦𝐵 ( 𝜑𝑦 = 𝑤 ) ) )
17 16 adantr ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝑧𝐴𝑤𝐵 ) ) → ( ∀ 𝑥𝐴𝑥𝐴𝑦𝐵 ( 𝜑𝑦 = 𝑤 ) ↔ ∀ 𝑥𝐴𝑦𝐵 ( 𝜑𝑦 = 𝑤 ) ) )
18 17 anbi2d ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝑧𝐴𝑤𝐵 ) ) → ( ( ∀ 𝑥𝐴𝑦𝐵 ( 𝜑𝑥 = 𝑧 ) ∧ ∀ 𝑥𝐴𝑥𝐴𝑦𝐵 ( 𝜑𝑦 = 𝑤 ) ) ↔ ( ∀ 𝑥𝐴𝑦𝐵 ( 𝜑𝑥 = 𝑧 ) ∧ ∀ 𝑥𝐴𝑦𝐵 ( 𝜑𝑦 = 𝑤 ) ) ) )
19 jcab ( ( 𝜑 → ( 𝑥 = 𝑧𝑦 = 𝑤 ) ) ↔ ( ( 𝜑𝑥 = 𝑧 ) ∧ ( 𝜑𝑦 = 𝑤 ) ) )
20 19 ralbii ( ∀ 𝑦𝐵 ( 𝜑 → ( 𝑥 = 𝑧𝑦 = 𝑤 ) ) ↔ ∀ 𝑦𝐵 ( ( 𝜑𝑥 = 𝑧 ) ∧ ( 𝜑𝑦 = 𝑤 ) ) )
21 r19.26 ( ∀ 𝑦𝐵 ( ( 𝜑𝑥 = 𝑧 ) ∧ ( 𝜑𝑦 = 𝑤 ) ) ↔ ( ∀ 𝑦𝐵 ( 𝜑𝑥 = 𝑧 ) ∧ ∀ 𝑦𝐵 ( 𝜑𝑦 = 𝑤 ) ) )
22 20 21 bitri ( ∀ 𝑦𝐵 ( 𝜑 → ( 𝑥 = 𝑧𝑦 = 𝑤 ) ) ↔ ( ∀ 𝑦𝐵 ( 𝜑𝑥 = 𝑧 ) ∧ ∀ 𝑦𝐵 ( 𝜑𝑦 = 𝑤 ) ) )
23 22 ralbii ( ∀ 𝑥𝐴𝑦𝐵 ( 𝜑 → ( 𝑥 = 𝑧𝑦 = 𝑤 ) ) ↔ ∀ 𝑥𝐴 ( ∀ 𝑦𝐵 ( 𝜑𝑥 = 𝑧 ) ∧ ∀ 𝑦𝐵 ( 𝜑𝑦 = 𝑤 ) ) )
24 r19.26 ( ∀ 𝑥𝐴 ( ∀ 𝑦𝐵 ( 𝜑𝑥 = 𝑧 ) ∧ ∀ 𝑦𝐵 ( 𝜑𝑦 = 𝑤 ) ) ↔ ( ∀ 𝑥𝐴𝑦𝐵 ( 𝜑𝑥 = 𝑧 ) ∧ ∀ 𝑥𝐴𝑦𝐵 ( 𝜑𝑦 = 𝑤 ) ) )
25 23 24 bitri ( ∀ 𝑥𝐴𝑦𝐵 ( 𝜑 → ( 𝑥 = 𝑧𝑦 = 𝑤 ) ) ↔ ( ∀ 𝑥𝐴𝑦𝐵 ( 𝜑𝑥 = 𝑧 ) ∧ ∀ 𝑥𝐴𝑦𝐵 ( 𝜑𝑦 = 𝑤 ) ) )
26 25 a1i ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝑧𝐴𝑤𝐵 ) ) → ( ∀ 𝑥𝐴𝑦𝐵 ( 𝜑 → ( 𝑥 = 𝑧𝑦 = 𝑤 ) ) ↔ ( ∀ 𝑥𝐴𝑦𝐵 ( 𝜑𝑥 = 𝑧 ) ∧ ∀ 𝑥𝐴𝑦𝐵 ( 𝜑𝑦 = 𝑤 ) ) ) )
27 18 26 bitr4d ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝑧𝐴𝑤𝐵 ) ) → ( ( ∀ 𝑥𝐴𝑦𝐵 ( 𝜑𝑥 = 𝑧 ) ∧ ∀ 𝑥𝐴𝑥𝐴𝑦𝐵 ( 𝜑𝑦 = 𝑤 ) ) ↔ ∀ 𝑥𝐴𝑦𝐵 ( 𝜑 → ( 𝑥 = 𝑧𝑦 = 𝑤 ) ) ) )
28 12 27 bitr2id ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝑧𝐴𝑤𝐵 ) ) → ( ∀ 𝑥𝐴𝑦𝐵 ( 𝜑 → ( 𝑥 = 𝑧𝑦 = 𝑤 ) ) ↔ ∀ 𝑥𝐴 ( ∀ 𝑦𝐵 ( 𝜑𝑥 = 𝑧 ) ∧ ∀ 𝑥𝐴𝑦𝐵 ( 𝜑𝑦 = 𝑤 ) ) ) )
29 r19.26 ( ∀ 𝑦𝐵 ( ∀ 𝑦𝐵 ( 𝜑𝑥 = 𝑧 ) ∧ ∀ 𝑥𝐴 ( 𝜑𝑦 = 𝑤 ) ) ↔ ( ∀ 𝑦𝐵𝑦𝐵 ( 𝜑𝑥 = 𝑧 ) ∧ ∀ 𝑦𝐵𝑥𝐴 ( 𝜑𝑦 = 𝑤 ) ) )
30 nfra1 𝑦𝑦𝐵 ( 𝜑𝑥 = 𝑧 )
31 30 r19.3rz ( 𝐵 ≠ ∅ → ( ∀ 𝑦𝐵 ( 𝜑𝑥 = 𝑧 ) ↔ ∀ 𝑦𝐵𝑦𝐵 ( 𝜑𝑥 = 𝑧 ) ) )
32 31 ad2antlr ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝑧𝐴𝑤𝐵 ) ) → ( ∀ 𝑦𝐵 ( 𝜑𝑥 = 𝑧 ) ↔ ∀ 𝑦𝐵𝑦𝐵 ( 𝜑𝑥 = 𝑧 ) ) )
33 32 bicomd ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝑧𝐴𝑤𝐵 ) ) → ( ∀ 𝑦𝐵𝑦𝐵 ( 𝜑𝑥 = 𝑧 ) ↔ ∀ 𝑦𝐵 ( 𝜑𝑥 = 𝑧 ) ) )
34 ralcom ( ∀ 𝑦𝐵𝑥𝐴 ( 𝜑𝑦 = 𝑤 ) ↔ ∀ 𝑥𝐴𝑦𝐵 ( 𝜑𝑦 = 𝑤 ) )
35 34 a1i ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝑧𝐴𝑤𝐵 ) ) → ( ∀ 𝑦𝐵𝑥𝐴 ( 𝜑𝑦 = 𝑤 ) ↔ ∀ 𝑥𝐴𝑦𝐵 ( 𝜑𝑦 = 𝑤 ) ) )
36 33 35 anbi12d ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝑧𝐴𝑤𝐵 ) ) → ( ( ∀ 𝑦𝐵𝑦𝐵 ( 𝜑𝑥 = 𝑧 ) ∧ ∀ 𝑦𝐵𝑥𝐴 ( 𝜑𝑦 = 𝑤 ) ) ↔ ( ∀ 𝑦𝐵 ( 𝜑𝑥 = 𝑧 ) ∧ ∀ 𝑥𝐴𝑦𝐵 ( 𝜑𝑦 = 𝑤 ) ) ) )
37 29 36 syl5bb ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝑧𝐴𝑤𝐵 ) ) → ( ∀ 𝑦𝐵 ( ∀ 𝑦𝐵 ( 𝜑𝑥 = 𝑧 ) ∧ ∀ 𝑥𝐴 ( 𝜑𝑦 = 𝑤 ) ) ↔ ( ∀ 𝑦𝐵 ( 𝜑𝑥 = 𝑧 ) ∧ ∀ 𝑥𝐴𝑦𝐵 ( 𝜑𝑦 = 𝑤 ) ) ) )
38 37 ralbidv ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝑧𝐴𝑤𝐵 ) ) → ( ∀ 𝑥𝐴𝑦𝐵 ( ∀ 𝑦𝐵 ( 𝜑𝑥 = 𝑧 ) ∧ ∀ 𝑥𝐴 ( 𝜑𝑦 = 𝑤 ) ) ↔ ∀ 𝑥𝐴 ( ∀ 𝑦𝐵 ( 𝜑𝑥 = 𝑧 ) ∧ ∀ 𝑥𝐴𝑦𝐵 ( 𝜑𝑦 = 𝑤 ) ) ) )
39 28 38 bitr4d ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝑧𝐴𝑤𝐵 ) ) → ( ∀ 𝑥𝐴𝑦𝐵 ( 𝜑 → ( 𝑥 = 𝑧𝑦 = 𝑤 ) ) ↔ ∀ 𝑥𝐴𝑦𝐵 ( ∀ 𝑦𝐵 ( 𝜑𝑥 = 𝑧 ) ∧ ∀ 𝑥𝐴 ( 𝜑𝑦 = 𝑤 ) ) ) )
40 r19.23v ( ∀ 𝑦𝐵 ( 𝜑𝑥 = 𝑧 ) ↔ ( ∃ 𝑦𝐵 𝜑𝑥 = 𝑧 ) )
41 r19.23v ( ∀ 𝑥𝐴 ( 𝜑𝑦 = 𝑤 ) ↔ ( ∃ 𝑥𝐴 𝜑𝑦 = 𝑤 ) )
42 40 41 anbi12i ( ( ∀ 𝑦𝐵 ( 𝜑𝑥 = 𝑧 ) ∧ ∀ 𝑥𝐴 ( 𝜑𝑦 = 𝑤 ) ) ↔ ( ( ∃ 𝑦𝐵 𝜑𝑥 = 𝑧 ) ∧ ( ∃ 𝑥𝐴 𝜑𝑦 = 𝑤 ) ) )
43 42 2ralbii ( ∀ 𝑥𝐴𝑦𝐵 ( ∀ 𝑦𝐵 ( 𝜑𝑥 = 𝑧 ) ∧ ∀ 𝑥𝐴 ( 𝜑𝑦 = 𝑤 ) ) ↔ ∀ 𝑥𝐴𝑦𝐵 ( ( ∃ 𝑦𝐵 𝜑𝑥 = 𝑧 ) ∧ ( ∃ 𝑥𝐴 𝜑𝑦 = 𝑤 ) ) )
44 43 a1i ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝑧𝐴𝑤𝐵 ) ) → ( ∀ 𝑥𝐴𝑦𝐵 ( ∀ 𝑦𝐵 ( 𝜑𝑥 = 𝑧 ) ∧ ∀ 𝑥𝐴 ( 𝜑𝑦 = 𝑤 ) ) ↔ ∀ 𝑥𝐴𝑦𝐵 ( ( ∃ 𝑦𝐵 𝜑𝑥 = 𝑧 ) ∧ ( ∃ 𝑥𝐴 𝜑𝑦 = 𝑤 ) ) ) )
45 neneq ( 𝐴 ≠ ∅ → ¬ 𝐴 = ∅ )
46 neneq ( 𝐵 ≠ ∅ → ¬ 𝐵 = ∅ )
47 45 46 anim12i ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) → ( ¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅ ) )
48 47 olcd ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) → ( ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ∨ ( ¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅ ) ) )
49 dfbi3 ( ( 𝐴 = ∅ ↔ 𝐵 = ∅ ) ↔ ( ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ∨ ( ¬ 𝐴 = ∅ ∧ ¬ 𝐵 = ∅ ) ) )
50 48 49 sylibr ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) → ( 𝐴 = ∅ ↔ 𝐵 = ∅ ) )
51 nfre1 𝑦𝑦𝐵 𝜑
52 nfv 𝑦 𝑥 = 𝑧
53 51 52 nfim 𝑦 ( ∃ 𝑦𝐵 𝜑𝑥 = 𝑧 )
54 nfre1 𝑥𝑥𝐴 𝜑
55 nfv 𝑥 𝑦 = 𝑤
56 54 55 nfim 𝑥 ( ∃ 𝑥𝐴 𝜑𝑦 = 𝑤 )
57 53 56 raaan2 ( ( 𝐴 = ∅ ↔ 𝐵 = ∅ ) → ( ∀ 𝑥𝐴𝑦𝐵 ( ( ∃ 𝑦𝐵 𝜑𝑥 = 𝑧 ) ∧ ( ∃ 𝑥𝐴 𝜑𝑦 = 𝑤 ) ) ↔ ( ∀ 𝑥𝐴 ( ∃ 𝑦𝐵 𝜑𝑥 = 𝑧 ) ∧ ∀ 𝑦𝐵 ( ∃ 𝑥𝐴 𝜑𝑦 = 𝑤 ) ) ) )
58 50 57 syl ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) → ( ∀ 𝑥𝐴𝑦𝐵 ( ( ∃ 𝑦𝐵 𝜑𝑥 = 𝑧 ) ∧ ( ∃ 𝑥𝐴 𝜑𝑦 = 𝑤 ) ) ↔ ( ∀ 𝑥𝐴 ( ∃ 𝑦𝐵 𝜑𝑥 = 𝑧 ) ∧ ∀ 𝑦𝐵 ( ∃ 𝑥𝐴 𝜑𝑦 = 𝑤 ) ) ) )
59 58 adantr ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝑧𝐴𝑤𝐵 ) ) → ( ∀ 𝑥𝐴𝑦𝐵 ( ( ∃ 𝑦𝐵 𝜑𝑥 = 𝑧 ) ∧ ( ∃ 𝑥𝐴 𝜑𝑦 = 𝑤 ) ) ↔ ( ∀ 𝑥𝐴 ( ∃ 𝑦𝐵 𝜑𝑥 = 𝑧 ) ∧ ∀ 𝑦𝐵 ( ∃ 𝑥𝐴 𝜑𝑦 = 𝑤 ) ) ) )
60 39 44 59 3bitrd ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝑧𝐴𝑤𝐵 ) ) → ( ∀ 𝑥𝐴𝑦𝐵 ( 𝜑 → ( 𝑥 = 𝑧𝑦 = 𝑤 ) ) ↔ ( ∀ 𝑥𝐴 ( ∃ 𝑦𝐵 𝜑𝑥 = 𝑧 ) ∧ ∀ 𝑦𝐵 ( ∃ 𝑥𝐴 𝜑𝑦 = 𝑤 ) ) ) )
61 60 2rexbidva ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) → ( ∃ 𝑧𝐴𝑤𝐵𝑥𝐴𝑦𝐵 ( 𝜑 → ( 𝑥 = 𝑧𝑦 = 𝑤 ) ) ↔ ∃ 𝑧𝐴𝑤𝐵 ( ∀ 𝑥𝐴 ( ∃ 𝑦𝐵 𝜑𝑥 = 𝑧 ) ∧ ∀ 𝑦𝐵 ( ∃ 𝑥𝐴 𝜑𝑦 = 𝑤 ) ) ) )
62 reeanv ( ∃ 𝑧𝐴𝑤𝐵 ( ∀ 𝑥𝐴 ( ∃ 𝑦𝐵 𝜑𝑥 = 𝑧 ) ∧ ∀ 𝑦𝐵 ( ∃ 𝑥𝐴 𝜑𝑦 = 𝑤 ) ) ↔ ( ∃ 𝑧𝐴𝑥𝐴 ( ∃ 𝑦𝐵 𝜑𝑥 = 𝑧 ) ∧ ∃ 𝑤𝐵𝑦𝐵 ( ∃ 𝑥𝐴 𝜑𝑦 = 𝑤 ) ) )
63 61 62 bitr2di ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) → ( ( ∃ 𝑧𝐴𝑥𝐴 ( ∃ 𝑦𝐵 𝜑𝑥 = 𝑧 ) ∧ ∃ 𝑤𝐵𝑦𝐵 ( ∃ 𝑥𝐴 𝜑𝑦 = 𝑤 ) ) ↔ ∃ 𝑧𝐴𝑤𝐵𝑥𝐴𝑦𝐵 ( 𝜑 → ( 𝑥 = 𝑧𝑦 = 𝑤 ) ) ) )
64 11 63 anbi12d ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) → ( ( ( ∃ 𝑥𝐴𝑦𝐵 𝜑 ∧ ∃ 𝑦𝐵𝑥𝐴 𝜑 ) ∧ ( ∃ 𝑧𝐴𝑥𝐴 ( ∃ 𝑦𝐵 𝜑𝑥 = 𝑧 ) ∧ ∃ 𝑤𝐵𝑦𝐵 ( ∃ 𝑥𝐴 𝜑𝑦 = 𝑤 ) ) ) ↔ ( ∃ 𝑥𝐴𝑦𝐵 𝜑 ∧ ∃ 𝑧𝐴𝑤𝐵𝑥𝐴𝑦𝐵 ( 𝜑 → ( 𝑥 = 𝑧𝑦 = 𝑤 ) ) ) ) )
65 4 6 64 3bitrd ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) → ( ( ∃! 𝑥𝐴𝑦𝐵 𝜑 ∧ ∃! 𝑦𝐵𝑥𝐴 𝜑 ) ↔ ( ∃ 𝑥𝐴𝑦𝐵 𝜑 ∧ ∃ 𝑧𝐴𝑤𝐵𝑥𝐴𝑦𝐵 ( 𝜑 → ( 𝑥 = 𝑧𝑦 = 𝑤 ) ) ) ) )