Metamath Proof Explorer

Theorem ichnreuop

Description: If the setvar variables are interchangeable in a wff, there is never a unique ordered pair with different components fulfilling the wff (because if <. a , b >. fulfils the wff, then also <. b , a >. fulfils the wff). (Contributed by AV, 27-Aug-2023)

Ref Expression
Assertion ichnreuop ( [ 𝑎 ⇄ 𝑏 ] 𝜑 → ¬ ∃! 𝑝 ∈ ( 𝑋 × 𝑋 ) ∃ 𝑎 ∃ 𝑏 ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) )

Proof

Step Hyp Ref Expression
1 notnotb ⊢ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) ↔ ¬ ¬ ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) )
2 nfv ⊢ Ⅎ 𝑐 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 )
3 nfv ⊢ Ⅎ 𝑑 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 )
4 nfv ⊢ Ⅎ 𝑎 ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑐 , 𝑑 ⟩
5 nfv ⊢ Ⅎ 𝑎 𝑐 ≠ 𝑑
6 nfsbc1v ⊢ Ⅎ 𝑎 [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑
7 4 5 6 nf3an ⊢ Ⅎ 𝑎 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑐 ≠ 𝑑 ∧ [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 )
8 nfv ⊢ Ⅎ 𝑏 ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑐 , 𝑑 ⟩
9 nfv ⊢ Ⅎ 𝑏 𝑐 ≠ 𝑑
10 nfcv ⊢ Ⅎ 𝑏 𝑐
11 nfsbc1v ⊢ Ⅎ 𝑏 [ 𝑑 / 𝑏 ] 𝜑
12 10 11 nfsbcw ⊢ Ⅎ 𝑏 [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑
13 8 9 12 nf3an ⊢ Ⅎ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑐 ≠ 𝑑 ∧ [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 )
14 opeq12 ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ )
15 14 eqeq2d ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ↔ ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ) )
16 simpl ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → 𝑎 = 𝑐 )
17 simpr ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → 𝑏 = 𝑑 )
18 16 17 neeq12d ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( 𝑎 ≠ 𝑏 ↔ 𝑐 ≠ 𝑑 ) )
19 sbceq1a ⊢ ( 𝑏 = 𝑑 → ( 𝜑 ↔ [ 𝑑 / 𝑏 ] 𝜑 ) )
20 sbceq1a ⊢ ( 𝑎 = 𝑐 → ( [ 𝑑 / 𝑏 ] 𝜑 ↔ [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 ) )
21 19 20 sylan9bbr ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( 𝜑 ↔ [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 ) )
22 15 18 21 3anbi123d ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑐 ≠ 𝑑 ∧ [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 ) ) )
23 2 3 7 13 22 cbvex2v ⊢ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) ↔ ∃ 𝑐 ∃ 𝑑 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑐 ≠ 𝑑 ∧ [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 ) )
24 vex ⊢ 𝑥 ∈ V
25 vex ⊢ 𝑦 ∈ V
26 24 25 opth ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ↔ ( 𝑥 = 𝑐 ∧ 𝑦 = 𝑑 ) )
27 eleq1w ⊢ ( 𝑦 = 𝑑 → ( 𝑦 ∈ 𝑋 ↔ 𝑑 ∈ 𝑋 ) )
28 27 biimpcd ⊢ ( 𝑦 ∈ 𝑋 → ( 𝑦 = 𝑑 → 𝑑 ∈ 𝑋 ) )
29 28 adantl ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑦 = 𝑑 → 𝑑 ∈ 𝑋 ) )
30 29 adantl ⊢ ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑦 = 𝑑 → 𝑑 ∈ 𝑋 ) )
31 30 com12 ⊢ ( 𝑦 = 𝑑 → ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑑 ∈ 𝑋 ) )
32 31 adantl ⊢ ( ( 𝑥 = 𝑐 ∧ 𝑦 = 𝑑 ) → ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑑 ∈ 𝑋 ) )
33 26 32 sylbi ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ → ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑑 ∈ 𝑋 ) )
34 33 3ad2ant1 ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑐 ≠ 𝑑 ∧ [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 ) → ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑑 ∈ 𝑋 ) )
35 34 impcom ⊢ ( ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑐 ≠ 𝑑 ∧ [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 ) ) → 𝑑 ∈ 𝑋 )
36 eleq1w ⊢ ( 𝑥 = 𝑐 → ( 𝑥 ∈ 𝑋 ↔ 𝑐 ∈ 𝑋 ) )
37 36 biimpcd ⊢ ( 𝑥 ∈ 𝑋 → ( 𝑥 = 𝑐 → 𝑐 ∈ 𝑋 ) )
38 37 adantr ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 = 𝑐 → 𝑐 ∈ 𝑋 ) )
39 38 adantl ⊢ ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 = 𝑐 → 𝑐 ∈ 𝑋 ) )
40 39 com12 ⊢ ( 𝑥 = 𝑐 → ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑐 ∈ 𝑋 ) )
41 40 adantr ⊢ ( ( 𝑥 = 𝑐 ∧ 𝑦 = 𝑑 ) → ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑐 ∈ 𝑋 ) )
42 26 41 sylbi ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ → ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑐 ∈ 𝑋 ) )
43 42 3ad2ant1 ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑐 ≠ 𝑑 ∧ [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 ) → ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑐 ∈ 𝑋 ) )
44 43 impcom ⊢ ( ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑐 ≠ 𝑑 ∧ [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 ) ) → 𝑐 ∈ 𝑋 )
45 eqidd ⊢ ( ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑐 ≠ 𝑑 ∧ [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 ) ) → ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑑 , 𝑐 ⟩ )
46 necom ⊢ ( 𝑐 ≠ 𝑑 ↔ 𝑑 ≠ 𝑐 )
47 46 biimpi ⊢ ( 𝑐 ≠ 𝑑 → 𝑑 ≠ 𝑐 )
48 47 3ad2ant2 ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑐 ≠ 𝑑 ∧ [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 ) → 𝑑 ≠ 𝑐 )
49 48 adantl ⊢ ( ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑐 ≠ 𝑑 ∧ [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 ) ) → 𝑑 ≠ 𝑐 )
50 dfich2 ⊢ ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ↔ ∀ 𝑐 ∀ 𝑑 ( [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 ↔ [ 𝑑 / 𝑎 ] [ 𝑐 / 𝑏 ] 𝜑 ) )
51 2sp ⊢ ( ∀ 𝑐 ∀ 𝑑 ( [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 ↔ [ 𝑑 / 𝑎 ] [ 𝑐 / 𝑏 ] 𝜑 ) → ( [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 ↔ [ 𝑑 / 𝑎 ] [ 𝑐 / 𝑏 ] 𝜑 ) )
52 sbsbc ⊢ ( [ 𝑑 / 𝑏 ] 𝜑 ↔ [ 𝑑 / 𝑏 ] 𝜑 )
53 52 sbbii ⊢ ( [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 ↔ [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 )
54 sbsbc ⊢ ( [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 ↔ [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 )
55 53 54 bitri ⊢ ( [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 ↔ [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 )
56 sbsbc ⊢ ( [ 𝑐 / 𝑏 ] 𝜑 ↔ [ 𝑐 / 𝑏 ] 𝜑 )
57 56 sbbii ⊢ ( [ 𝑑 / 𝑎 ] [ 𝑐 / 𝑏 ] 𝜑 ↔ [ 𝑑 / 𝑎 ] [ 𝑐 / 𝑏 ] 𝜑 )
58 sbsbc ⊢ ( [ 𝑑 / 𝑎 ] [ 𝑐 / 𝑏 ] 𝜑 ↔ [ 𝑑 / 𝑎 ] [ 𝑐 / 𝑏 ] 𝜑 )
59 57 58 bitri ⊢ ( [ 𝑑 / 𝑎 ] [ 𝑐 / 𝑏 ] 𝜑 ↔ [ 𝑑 / 𝑎 ] [ 𝑐 / 𝑏 ] 𝜑 )
60 51 55 59 3bitr3g ⊢ ( ∀ 𝑐 ∀ 𝑑 ( [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 ↔ [ 𝑑 / 𝑎 ] [ 𝑐 / 𝑏 ] 𝜑 ) → ( [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 ↔ [ 𝑑 / 𝑎 ] [ 𝑐 / 𝑏 ] 𝜑 ) )
61 60 biimpd ⊢ ( ∀ 𝑐 ∀ 𝑑 ( [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 ↔ [ 𝑑 / 𝑎 ] [ 𝑐 / 𝑏 ] 𝜑 ) → ( [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 → [ 𝑑 / 𝑎 ] [ 𝑐 / 𝑏 ] 𝜑 ) )
62 50 61 sylbi ⊢ ( [ 𝑎 ⇄ 𝑏 ] 𝜑 → ( [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 → [ 𝑑 / 𝑎 ] [ 𝑐 / 𝑏 ] 𝜑 ) )
63 62 adantr ⊢ ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 → [ 𝑑 / 𝑎 ] [ 𝑐 / 𝑏 ] 𝜑 ) )
64 63 com12 ⊢ ( [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 → ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → [ 𝑑 / 𝑎 ] [ 𝑐 / 𝑏 ] 𝜑 ) )
65 64 3ad2ant3 ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑐 ≠ 𝑑 ∧ [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 ) → ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → [ 𝑑 / 𝑎 ] [ 𝑐 / 𝑏 ] 𝜑 ) )
66 65 impcom ⊢ ( ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑐 ≠ 𝑑 ∧ [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 ) ) → [ 𝑑 / 𝑎 ] [ 𝑐 / 𝑏 ] 𝜑 )
67 sbccom ⊢ ( [ 𝑐 / 𝑏 ] [ 𝑑 / 𝑎 ] 𝜑 ↔ [ 𝑑 / 𝑎 ] [ 𝑐 / 𝑏 ] 𝜑 )
68 66 67 sylibr ⊢ ( ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑐 ≠ 𝑑 ∧ [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 ) ) → [ 𝑐 / 𝑏 ] [ 𝑑 / 𝑎 ] 𝜑 )
69 45 49 68 3jca ⊢ ( ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑐 ≠ 𝑑 ∧ [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 ) ) → ( ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑑 , 𝑐 ⟩ ∧ 𝑑 ≠ 𝑐 ∧ [ 𝑐 / 𝑏 ] [ 𝑑 / 𝑎 ] 𝜑 ) )
70 nfv ⊢ Ⅎ 𝑏 ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑑 , 𝑐 ⟩
71 nfv ⊢ Ⅎ 𝑏 𝑑 ≠ 𝑐
72 nfsbc1v ⊢ Ⅎ 𝑏 [ 𝑐 / 𝑏 ] [ 𝑑 / 𝑎 ] 𝜑
73 70 71 72 nf3an ⊢ Ⅎ 𝑏 ( ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑑 , 𝑐 ⟩ ∧ 𝑑 ≠ 𝑐 ∧ [ 𝑐 / 𝑏 ] [ 𝑑 / 𝑎 ] 𝜑 )
74 opeq2 ⊢ ( 𝑏 = 𝑐 → ⟨ 𝑑 , 𝑏 ⟩ = ⟨ 𝑑 , 𝑐 ⟩ )
75 74 eqeq2d ⊢ ( 𝑏 = 𝑐 → ( ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑑 , 𝑏 ⟩ ↔ ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑑 , 𝑐 ⟩ ) )
76 neeq2 ⊢ ( 𝑏 = 𝑐 → ( 𝑑 ≠ 𝑏 ↔ 𝑑 ≠ 𝑐 ) )
77 sbceq1a ⊢ ( 𝑏 = 𝑐 → ( [ 𝑑 / 𝑎 ] 𝜑 ↔ [ 𝑐 / 𝑏 ] [ 𝑑 / 𝑎 ] 𝜑 ) )
78 75 76 77 3anbi123d ⊢ ( 𝑏 = 𝑐 → ( ( ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑑 , 𝑏 ⟩ ∧ 𝑑 ≠ 𝑏 ∧ [ 𝑑 / 𝑎 ] 𝜑 ) ↔ ( ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑑 , 𝑐 ⟩ ∧ 𝑑 ≠ 𝑐 ∧ [ 𝑐 / 𝑏 ] [ 𝑑 / 𝑎 ] 𝜑 ) ) )
79 10 73 78 spcegf ⊢ ( 𝑐 ∈ 𝑋 → ( ( ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑑 , 𝑐 ⟩ ∧ 𝑑 ≠ 𝑐 ∧ [ 𝑐 / 𝑏 ] [ 𝑑 / 𝑎 ] 𝜑 ) → ∃ 𝑏 ( ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑑 , 𝑏 ⟩ ∧ 𝑑 ≠ 𝑏 ∧ [ 𝑑 / 𝑎 ] 𝜑 ) ) )
80 44 69 79 sylc ⊢ ( ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑐 ≠ 𝑑 ∧ [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 ) ) → ∃ 𝑏 ( ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑑 , 𝑏 ⟩ ∧ 𝑑 ≠ 𝑏 ∧ [ 𝑑 / 𝑎 ] 𝜑 ) )
81 nfcv ⊢ Ⅎ 𝑎 𝑑
82 nfv ⊢ Ⅎ 𝑎 ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑑 , 𝑏 ⟩
83 nfv ⊢ Ⅎ 𝑎 𝑑 ≠ 𝑏
84 nfsbc1v ⊢ Ⅎ 𝑎 [ 𝑑 / 𝑎 ] 𝜑
85 82 83 84 nf3an ⊢ Ⅎ 𝑎 ( ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑑 , 𝑏 ⟩ ∧ 𝑑 ≠ 𝑏 ∧ [ 𝑑 / 𝑎 ] 𝜑 )
86 85 nfex ⊢ Ⅎ 𝑎 ∃ 𝑏 ( ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑑 , 𝑏 ⟩ ∧ 𝑑 ≠ 𝑏 ∧ [ 𝑑 / 𝑎 ] 𝜑 )
87 opeq1 ⊢ ( 𝑎 = 𝑑 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑑 , 𝑏 ⟩ )
88 87 eqeq2d ⊢ ( 𝑎 = 𝑑 → ( ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ↔ ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑑 , 𝑏 ⟩ ) )
89 neeq1 ⊢ ( 𝑎 = 𝑑 → ( 𝑎 ≠ 𝑏 ↔ 𝑑 ≠ 𝑏 ) )
90 sbceq1a ⊢ ( 𝑎 = 𝑑 → ( 𝜑 ↔ [ 𝑑 / 𝑎 ] 𝜑 ) )
91 88 89 90 3anbi123d ⊢ ( 𝑎 = 𝑑 → ( ( ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) ↔ ( ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑑 , 𝑏 ⟩ ∧ 𝑑 ≠ 𝑏 ∧ [ 𝑑 / 𝑎 ] 𝜑 ) ) )
92 91 exbidv ⊢ ( 𝑎 = 𝑑 → ( ∃ 𝑏 ( ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) ↔ ∃ 𝑏 ( ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑑 , 𝑏 ⟩ ∧ 𝑑 ≠ 𝑏 ∧ [ 𝑑 / 𝑎 ] 𝜑 ) ) )
93 81 86 92 spcegf ⊢ ( 𝑑 ∈ 𝑋 → ( ∃ 𝑏 ( ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑑 , 𝑏 ⟩ ∧ 𝑑 ≠ 𝑏 ∧ [ 𝑑 / 𝑎 ] 𝜑 ) → ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) ) )
94 35 80 93 sylc ⊢ ( ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑐 ≠ 𝑑 ∧ [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 ) ) → ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) )
95 vex ⊢ 𝑑 ∈ V
96 vex ⊢ 𝑐 ∈ V
97 95 96 opth1 ⊢ ( ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ → 𝑑 = 𝑐 )
98 97 equcomd ⊢ ( ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ → 𝑐 = 𝑑 )
99 98 necon3ai ⊢ ( 𝑐 ≠ 𝑑 → ¬ ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ )
100 99 adantl ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑐 ≠ 𝑑 ) → ¬ ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ )
101 eqeq2 ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ → ( ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ) )
102 101 adantr ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑐 ≠ 𝑑 ) → ( ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ) )
103 100 102 mtbird ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑐 ≠ 𝑑 ) → ¬ ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
104 103 3adant3 ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑐 ≠ 𝑑 ∧ [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 ) → ¬ ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
105 104 adantl ⊢ ( ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑐 ≠ 𝑑 ∧ [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 ) ) → ¬ ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
106 94 105 jcnd ⊢ ( ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑐 ≠ 𝑑 ∧ [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 ) ) → ¬ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) → ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) )
107 opeq1 ⊢ ( 𝑣 = 𝑑 → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑑 , 𝑤 ⟩ )
108 107 eqeq1d ⊢ ( 𝑣 = 𝑑 → ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ↔ ⟨ 𝑑 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) )
109 108 3anbi1d ⊢ ( 𝑣 = 𝑑 → ( ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) ↔ ( ⟨ 𝑑 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) ) )
110 109 2exbidv ⊢ ( 𝑣 = 𝑑 → ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) ↔ ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑑 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) ) )
111 107 eqeq1d ⊢ ( 𝑣 = 𝑑 → ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝑑 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) )
112 110 111 imbi12d ⊢ ( 𝑣 = 𝑑 → ( ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑑 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) → ⟨ 𝑑 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
113 112 notbid ⊢ ( 𝑣 = 𝑑 → ( ¬ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ¬ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑑 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) → ⟨ 𝑑 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
114 opeq2 ⊢ ( 𝑤 = 𝑐 → ⟨ 𝑑 , 𝑤 ⟩ = ⟨ 𝑑 , 𝑐 ⟩ )
115 114 eqeq1d ⊢ ( 𝑤 = 𝑐 → ( ⟨ 𝑑 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ↔ ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) )
116 115 3anbi1d ⊢ ( 𝑤 = 𝑐 → ( ( ⟨ 𝑑 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) ↔ ( ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) ) )
117 116 2exbidv ⊢ ( 𝑤 = 𝑐 → ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑑 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) ↔ ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) ) )
118 114 eqeq1d ⊢ ( 𝑤 = 𝑐 → ( ⟨ 𝑑 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) )
119 117 118 imbi12d ⊢ ( 𝑤 = 𝑐 → ( ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑑 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) → ⟨ 𝑑 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) → ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
120 119 notbid ⊢ ( 𝑤 = 𝑐 → ( ¬ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑑 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) → ⟨ 𝑑 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ¬ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) → ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
121 113 120 rspc2ev ⊢ ( ( 𝑑 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ∧ ¬ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) → ⟨ 𝑑 , 𝑐 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) → ∃ 𝑣 ∈ 𝑋 ∃ 𝑤 ∈ 𝑋 ¬ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) )
122 35 44 106 121 syl3anc ⊢ ( ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑐 ≠ 𝑑 ∧ [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 ) ) → ∃ 𝑣 ∈ 𝑋 ∃ 𝑤 ∈ 𝑋 ¬ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) )
123 rexnal2 ⊢ ( ∃ 𝑣 ∈ 𝑋 ∃ 𝑤 ∈ 𝑋 ¬ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ¬ ∀ 𝑣 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) )
124 122 123 sylib ⊢ ( ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑐 ≠ 𝑑 ∧ [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 ) ) → ¬ ∀ 𝑣 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) )
125 124 ex ⊢ ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑐 ≠ 𝑑 ∧ [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 ) → ¬ ∀ 𝑣 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
126 125 exlimdvv ⊢ ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ∃ 𝑐 ∃ 𝑑 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑐 ≠ 𝑑 ∧ [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 ) → ¬ ∀ 𝑣 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
127 23 126 biimtrid ⊢ ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) → ¬ ∀ 𝑣 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
128 1 127 biimtrrid ⊢ ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ¬ ¬ ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) → ¬ ∀ 𝑣 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
129 128 orrd ⊢ ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ¬ ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) ∨ ¬ ∀ 𝑣 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
130 ianor ⊢ ( ¬ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) ∧ ∀ 𝑣 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) ↔ ( ¬ ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) ∨ ¬ ∀ 𝑣 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
131 129 130 sylibr ⊢ ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ¬ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) ∧ ∀ 𝑣 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
132 131 ralrimivva ⊢ ( [ 𝑎 ⇄ 𝑏 ] 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ¬ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) ∧ ∀ 𝑣 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
133 ralnex2 ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ¬ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) ∧ ∀ 𝑣 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) ↔ ¬ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) ∧ ∀ 𝑣 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
134 132 133 sylib ⊢ ( [ 𝑎 ⇄ 𝑏 ] 𝜑 → ¬ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) ∧ ∀ 𝑣 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
135 eqeq1 ⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ↔ ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) )
136 135 3anbi1d ⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) ) )
137 136 2exbidv ⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( ∃ 𝑎 ∃ 𝑏 ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) ↔ ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) ) )
138 eqeq1 ⊢ ( 𝑝 = ⟨ 𝑣 , 𝑤 ⟩ → ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ↔ ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) )
139 138 3anbi1d ⊢ ( 𝑝 = ⟨ 𝑣 , 𝑤 ⟩ → ( ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) ↔ ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) ) )
140 139 2exbidv ⊢ ( 𝑝 = ⟨ 𝑣 , 𝑤 ⟩ → ( ∃ 𝑎 ∃ 𝑏 ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) ↔ ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) ) )
141 137 140 reuop ⊢ ( ∃! 𝑝 ∈ ( 𝑋 × 𝑋 ) ∃ 𝑎 ∃ 𝑏 ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) ↔ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) ∧ ∀ 𝑣 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) → ⟨ 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) ) )
142 134 141 sylnibr ⊢ ( [ 𝑎 ⇄ 𝑏 ] 𝜑 → ¬ ∃! 𝑝 ∈ ( 𝑋 × 𝑋 ) ∃ 𝑎 ∃ 𝑏 ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑 ) )