This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 bitrid ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) → ( ∀ 𝑦 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝑧 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝑦 = 𝑤 ) ) ↔ ( ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝑧 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑦 = 𝑤 ) ) ) )
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 ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) → ( ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) ↔ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) ) )