Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  reuopreuprim Structured version   Visualization version   GIF version

Theorem reuopreuprim 44559
Description: There is a unique unordered pair with ordered elements fulfilling a wff if there is a unique ordered pair fulfilling the wff. (Contributed by AV, 28-Jul-2023.)
Assertion
Ref Expression
reuopreuprim (𝑋𝑉 → (∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ∃!𝑝 ∈ (Pairs‘𝑋)∃𝑎𝑏(𝑝 = {𝑎, 𝑏} ∧ 𝜑)))
Distinct variable groups:   𝑉,𝑝   𝑋,𝑎,𝑏,𝑝   𝜑,𝑝
Allowed substitution hints:   𝜑(𝑎,𝑏)   𝑉(𝑎,𝑏)

Proof of Theorem reuopreuprim
Dummy variables 𝑚 𝑛 𝑣 𝑤 𝑖 𝑗 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqeq1 2743 . . . . 5 (𝑝 = ⟨𝑥, 𝑦⟩ → (𝑝 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))
21anbi1d 633 . . . 4 (𝑝 = ⟨𝑥, 𝑦⟩ → ((𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
322exbidv 1931 . . 3 (𝑝 = ⟨𝑥, 𝑦⟩ → (∃𝑎𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
4 eqeq1 2743 . . . . 5 (𝑝 = ⟨𝑖, 𝑗⟩ → (𝑝 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩))
54anbi1d 633 . . . 4 (𝑝 = ⟨𝑖, 𝑗⟩ → ((𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
652exbidv 1931 . . 3 (𝑝 = ⟨𝑖, 𝑗⟩ → (∃𝑎𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
73, 6reuop 6135 . 2 (∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑥𝑋𝑦𝑋 (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖𝑋𝑗𝑋 (∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)))
8 simpll 767 . . . . . 6 (((𝑥𝑋𝑦𝑋) ∧ (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖𝑋𝑗𝑋 (∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) → 𝑥𝑋)
9 simplr 769 . . . . . 6 (((𝑥𝑋𝑦𝑋) ∧ (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖𝑋𝑗𝑋 (∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) → 𝑦𝑋)
10 oppr 44103 . . . . . . . . . . 11 ((𝑥 ∈ V ∧ 𝑦 ∈ V) → (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ → {𝑥, 𝑦} = {𝑎, 𝑏}))
1110el2v 3408 . . . . . . . . . 10 (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ → {𝑥, 𝑦} = {𝑎, 𝑏})
1211anim1i 618 . . . . . . . . 9 ((⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ({𝑥, 𝑦} = {𝑎, 𝑏} ∧ 𝜑))
13122eximi 1842 . . . . . . . 8 (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ∃𝑎𝑏({𝑥, 𝑦} = {𝑎, 𝑏} ∧ 𝜑))
1413adantr 484 . . . . . . 7 ((∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖𝑋𝑗𝑋 (∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)) → ∃𝑎𝑏({𝑥, 𝑦} = {𝑎, 𝑏} ∧ 𝜑))
1514adantl 485 . . . . . 6 (((𝑥𝑋𝑦𝑋) ∧ (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖𝑋𝑗𝑋 (∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) → ∃𝑎𝑏({𝑥, 𝑦} = {𝑎, 𝑏} ∧ 𝜑))
16 nfv 1921 . . . . . . . . . 10 𝑎(𝑥𝑋𝑦𝑋)
17 nfe1 2155 . . . . . . . . . . 11 𝑎𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)
18 nfcv 2900 . . . . . . . . . . . 12 𝑎𝑋
19 nfe1 2155 . . . . . . . . . . . . . 14 𝑎𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)
20 nfv 1921 . . . . . . . . . . . . . 14 𝑎𝑖, 𝑗⟩ = ⟨𝑥, 𝑦
2119, 20nfim 1903 . . . . . . . . . . . . 13 𝑎(∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)
2218, 21nfralw 3139 . . . . . . . . . . . 12 𝑎𝑗𝑋 (∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)
2318, 22nfralw 3139 . . . . . . . . . . 11 𝑎𝑖𝑋𝑗𝑋 (∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)
2417, 23nfan 1906 . . . . . . . . . 10 𝑎(∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖𝑋𝑗𝑋 (∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))
2516, 24nfan 1906 . . . . . . . . 9 𝑎((𝑥𝑋𝑦𝑋) ∧ (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖𝑋𝑗𝑋 (∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)))
26 nfv 1921 . . . . . . . . 9 𝑎(𝑚𝑋𝑛𝑋)
2725, 26nfan 1906 . . . . . . . 8 𝑎(((𝑥𝑋𝑦𝑋) ∧ (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖𝑋𝑗𝑋 (∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) ∧ (𝑚𝑋𝑛𝑋))
28 nfv 1921 . . . . . . . 8 𝑎{𝑚, 𝑛} = {𝑥, 𝑦}
29 nfv 1921 . . . . . . . . . . 11 𝑏(𝑥𝑋𝑦𝑋)
30 nfe1 2155 . . . . . . . . . . . . 13 𝑏𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)
3130nfex 2327 . . . . . . . . . . . 12 𝑏𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)
32 nfcv 2900 . . . . . . . . . . . . 13 𝑏𝑋
33 nfe1 2155 . . . . . . . . . . . . . . . 16 𝑏𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)
3433nfex 2327 . . . . . . . . . . . . . . 15 𝑏𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)
35 nfv 1921 . . . . . . . . . . . . . . 15 𝑏𝑖, 𝑗⟩ = ⟨𝑥, 𝑦
3634, 35nfim 1903 . . . . . . . . . . . . . 14 𝑏(∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)
3732, 36nfralw 3139 . . . . . . . . . . . . 13 𝑏𝑗𝑋 (∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)
3832, 37nfralw 3139 . . . . . . . . . . . 12 𝑏𝑖𝑋𝑗𝑋 (∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)
3931, 38nfan 1906 . . . . . . . . . . 11 𝑏(∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖𝑋𝑗𝑋 (∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))
4029, 39nfan 1906 . . . . . . . . . 10 𝑏((𝑥𝑋𝑦𝑋) ∧ (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖𝑋𝑗𝑋 (∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)))
41 nfv 1921 . . . . . . . . . 10 𝑏(𝑚𝑋𝑛𝑋)
4240, 41nfan 1906 . . . . . . . . 9 𝑏(((𝑥𝑋𝑦𝑋) ∧ (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖𝑋𝑗𝑋 (∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) ∧ (𝑚𝑋𝑛𝑋))
43 nfv 1921 . . . . . . . . 9 𝑏{𝑚, 𝑛} = {𝑥, 𝑦}
44 vex 3404 . . . . . . . . . . . 12 𝑚 ∈ V
45 vex 3404 . . . . . . . . . . . 12 𝑛 ∈ V
46 vex 3404 . . . . . . . . . . . 12 𝑎 ∈ V
47 vex 3404 . . . . . . . . . . . 12 𝑏 ∈ V
4844, 45, 46, 47preq12b 4746 . . . . . . . . . . 11 ({𝑚, 𝑛} = {𝑎, 𝑏} ↔ ((𝑚 = 𝑎𝑛 = 𝑏) ∨ (𝑚 = 𝑏𝑛 = 𝑎)))
49 opeq1 4769 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 𝑚 → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑗⟩)
5049eqeq1d 2741 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑚 → (⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑚, 𝑗⟩ = ⟨𝑎, 𝑏⟩))
5150anbi1d 633 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑚 → ((⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑚, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
52512exbidv 1931 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑚 → (∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑎𝑏(⟨𝑚, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
5349eqeq1d 2741 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑚 → (⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑚, 𝑗⟩ = ⟨𝑥, 𝑦⟩))
5452, 53imbi12d 348 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑚 → ((∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) ↔ (∃𝑎𝑏(⟨𝑚, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑗⟩ = ⟨𝑥, 𝑦⟩)))
55 opeq2 4771 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑛 → ⟨𝑚, 𝑗⟩ = ⟨𝑚, 𝑛⟩)
5655eqeq1d 2741 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑛 → (⟨𝑚, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩))
5756anbi1d 633 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑛 → ((⟨𝑚, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
58572exbidv 1931 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑛 → (∃𝑎𝑏(⟨𝑚, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑎𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
5955eqeq1d 2741 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑛 → (⟨𝑚, 𝑗⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩))
6058, 59imbi12d 348 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑛 → ((∃𝑎𝑏(⟨𝑚, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑗⟩ = ⟨𝑥, 𝑦⟩) ↔ (∃𝑎𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩)))
6154, 60rspc2v 3539 . . . . . . . . . . . . . . . 16 ((𝑚𝑋𝑛𝑋) → (∀𝑖𝑋𝑗𝑋 (∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) → (∃𝑎𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩)))
62 pm3.22 463 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑚𝑋𝑛𝑋) ∧ (𝑥𝑋𝑦𝑋)) → ((𝑥𝑋𝑦𝑋) ∧ (𝑚𝑋𝑛𝑋)))
63623adant2 1132 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑚𝑋𝑛𝑋) ∧ (𝑚 = 𝑎𝑛 = 𝑏) ∧ (𝑥𝑋𝑦𝑋)) → ((𝑥𝑋𝑦𝑋) ∧ (𝑚𝑋𝑛𝑋)))
6463adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑚𝑋𝑛𝑋) ∧ (𝑚 = 𝑎𝑛 = 𝑏) ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝜑) → ((𝑥𝑋𝑦𝑋) ∧ (𝑚𝑋𝑛𝑋)))
65 eqidd 2740 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑚𝑋𝑛𝑋) ∧ (𝑚 = 𝑎𝑛 = 𝑏) ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩)
66 sbceq1a 3696 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = 𝑚 → (𝜑[𝑚 / 𝑎]𝜑))
6766equcoms 2032 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑚 = 𝑎 → (𝜑[𝑚 / 𝑎]𝜑))
68 sbceq1a 3696 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 = 𝑛 → ([𝑚 / 𝑎]𝜑[𝑛 / 𝑏][𝑚 / 𝑎]𝜑))
6968equcoms 2032 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = 𝑏 → ([𝑚 / 𝑎]𝜑[𝑛 / 𝑏][𝑚 / 𝑎]𝜑))
7067, 69sylan9bb 513 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑚 = 𝑎𝑛 = 𝑏) → (𝜑[𝑛 / 𝑏][𝑚 / 𝑎]𝜑))
71703ad2ant2 1135 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑚𝑋𝑛𝑋) ∧ (𝑚 = 𝑎𝑛 = 𝑏) ∧ (𝑥𝑋𝑦𝑋)) → (𝜑[𝑛 / 𝑏][𝑚 / 𝑎]𝜑))
7271biimpa 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑚𝑋𝑛𝑋) ∧ (𝑚 = 𝑎𝑛 = 𝑏) ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝜑) → [𝑛 / 𝑏][𝑚 / 𝑎]𝜑)
7364, 65, 72jca32 519 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑚𝑋𝑛𝑋) ∧ (𝑚 = 𝑎𝑛 = 𝑏) ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝜑) → (((𝑥𝑋𝑦𝑋) ∧ (𝑚𝑋𝑛𝑋)) ∧ (⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩ ∧ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑)))
74 nfv 1921 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑎𝑚, 𝑛⟩ = ⟨𝑚, 𝑛
75 nfcv 2900 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑎𝑛
76 nfsbc1v 3705 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑎[𝑚 / 𝑎]𝜑
7775, 76nfsbcw 3707 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑎[𝑛 / 𝑏][𝑚 / 𝑎]𝜑
7874, 77nfan 1906 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑎(⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩ ∧ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑)
79 nfv 1921 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑏𝑚, 𝑛⟩ = ⟨𝑚, 𝑛
80 nfsbc1v 3705 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑏[𝑛 / 𝑏][𝑚 / 𝑎]𝜑
8179, 80nfan 1906 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩ ∧ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑)
82 opeq12 4773 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑎 = 𝑚𝑏 = 𝑛) → ⟨𝑎, 𝑏⟩ = ⟨𝑚, 𝑛⟩)
8382eqeq2d 2750 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 = 𝑚𝑏 = 𝑛) → (⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩))
8466, 68sylan9bb 513 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 = 𝑚𝑏 = 𝑛) → (𝜑[𝑛 / 𝑏][𝑚 / 𝑎]𝜑))
8583, 84anbi12d 634 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 = 𝑚𝑏 = 𝑛) → ((⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩ ∧ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑)))
8685adantl 485 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑥𝑋𝑦𝑋) ∧ (𝑎 = 𝑚𝑏 = 𝑛)) → ((⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩ ∧ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑)))
8778, 81, 86spc2ed 3508 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥𝑋𝑦𝑋) ∧ (𝑚𝑋𝑛𝑋)) → ((⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩ ∧ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑) → ∃𝑎𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
8887imp 410 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑥𝑋𝑦𝑋) ∧ (𝑚𝑋𝑛𝑋)) ∧ (⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩ ∧ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑)) → ∃𝑎𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑))
89 pm2.27 42 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑎𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ((∃𝑎𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩))
9073, 88, 893syl 18 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑚𝑋𝑛𝑋) ∧ (𝑚 = 𝑎𝑛 = 𝑏) ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝜑) → ((∃𝑎𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩))
91 oppr 44103 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑚 ∈ V ∧ 𝑛 ∈ V) → (⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩ → {𝑚, 𝑛} = {𝑥, 𝑦}))
9291el2v 3408 . . . . . . . . . . . . . . . . . . . . 21 (⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩ → {𝑚, 𝑛} = {𝑥, 𝑦})
9390, 92syl6 35 . . . . . . . . . . . . . . . . . . . 20 ((((𝑚𝑋𝑛𝑋) ∧ (𝑚 = 𝑎𝑛 = 𝑏) ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝜑) → ((∃𝑎𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩) → {𝑚, 𝑛} = {𝑥, 𝑦}))
9493ex 416 . . . . . . . . . . . . . . . . . . 19 (((𝑚𝑋𝑛𝑋) ∧ (𝑚 = 𝑎𝑛 = 𝑏) ∧ (𝑥𝑋𝑦𝑋)) → (𝜑 → ((∃𝑎𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩) → {𝑚, 𝑛} = {𝑥, 𝑦})))
9594com23 86 . . . . . . . . . . . . . . . . . 18 (((𝑚𝑋𝑛𝑋) ∧ (𝑚 = 𝑎𝑛 = 𝑏) ∧ (𝑥𝑋𝑦𝑋)) → ((∃𝑎𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))
96953exp 1120 . . . . . . . . . . . . . . . . 17 ((𝑚𝑋𝑛𝑋) → ((𝑚 = 𝑎𝑛 = 𝑏) → ((𝑥𝑋𝑦𝑋) → ((∃𝑎𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))))
9796com24 95 . . . . . . . . . . . . . . . 16 ((𝑚𝑋𝑛𝑋) → ((∃𝑎𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩) → ((𝑥𝑋𝑦𝑋) → ((𝑚 = 𝑎𝑛 = 𝑏) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))))
9861, 97syld 47 . . . . . . . . . . . . . . 15 ((𝑚𝑋𝑛𝑋) → (∀𝑖𝑋𝑗𝑋 (∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) → ((𝑥𝑋𝑦𝑋) → ((𝑚 = 𝑎𝑛 = 𝑏) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))))
9998com13 88 . . . . . . . . . . . . . 14 ((𝑥𝑋𝑦𝑋) → (∀𝑖𝑋𝑗𝑋 (∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) → ((𝑚𝑋𝑛𝑋) → ((𝑚 = 𝑎𝑛 = 𝑏) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))))
10099a1d 25 . . . . . . . . . . . . 13 ((𝑥𝑋𝑦𝑋) → (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → (∀𝑖𝑋𝑗𝑋 (∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) → ((𝑚𝑋𝑛𝑋) → ((𝑚 = 𝑎𝑛 = 𝑏) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦}))))))
101100imp42 430 . . . . . . . . . . . 12 ((((𝑥𝑋𝑦𝑋) ∧ (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖𝑋𝑗𝑋 (∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) ∧ (𝑚𝑋𝑛𝑋)) → ((𝑚 = 𝑎𝑛 = 𝑏) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))
102 opeq1 4769 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = 𝑛 → ⟨𝑖, 𝑗⟩ = ⟨𝑛, 𝑗⟩)
103102eqeq1d 2741 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 𝑛 → (⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑛, 𝑗⟩ = ⟨𝑎, 𝑏⟩))
104103anbi1d 633 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑛 → ((⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑛, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
1051042exbidv 1931 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑛 → (∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑎𝑏(⟨𝑛, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
106102eqeq1d 2741 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑛 → (⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑛, 𝑗⟩ = ⟨𝑥, 𝑦⟩))
107105, 106imbi12d 348 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑛 → ((∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) ↔ (∃𝑎𝑏(⟨𝑛, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑗⟩ = ⟨𝑥, 𝑦⟩)))
108 opeq2 4771 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑚 → ⟨𝑛, 𝑗⟩ = ⟨𝑛, 𝑚⟩)
109108eqeq1d 2741 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑚 → (⟨𝑛, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩))
110109anbi1d 633 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑚 → ((⟨𝑛, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
1111102exbidv 1931 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑚 → (∃𝑎𝑏(⟨𝑛, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑎𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
112108eqeq1d 2741 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑚 → (⟨𝑛, 𝑗⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩))
113111, 112imbi12d 348 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑚 → ((∃𝑎𝑏(⟨𝑛, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑗⟩ = ⟨𝑥, 𝑦⟩) ↔ (∃𝑎𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩)))
114107, 113rspc2v 3539 . . . . . . . . . . . . . . . . 17 ((𝑛𝑋𝑚𝑋) → (∀𝑖𝑋𝑗𝑋 (∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) → (∃𝑎𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩)))
115114ancoms 462 . . . . . . . . . . . . . . . 16 ((𝑚𝑋𝑛𝑋) → (∀𝑖𝑋𝑗𝑋 (∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) → (∃𝑎𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩)))
116 pm3.22 463 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑚𝑋𝑛𝑋) → (𝑛𝑋𝑚𝑋))
117116anim1ci 619 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑚𝑋𝑛𝑋) ∧ (𝑥𝑋𝑦𝑋)) → ((𝑥𝑋𝑦𝑋) ∧ (𝑛𝑋𝑚𝑋)))
1181173adant2 1132 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑚𝑋𝑛𝑋) ∧ (𝑚 = 𝑏𝑛 = 𝑎) ∧ (𝑥𝑋𝑦𝑋)) → ((𝑥𝑋𝑦𝑋) ∧ (𝑛𝑋𝑚𝑋)))
119118adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑚𝑋𝑛𝑋) ∧ (𝑚 = 𝑏𝑛 = 𝑎) ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝜑) → ((𝑥𝑋𝑦𝑋) ∧ (𝑛𝑋𝑚𝑋)))
120 eqidd 2740 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑚𝑋𝑛𝑋) ∧ (𝑚 = 𝑏𝑛 = 𝑎) ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩)
121 sbceq1a 3696 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 = 𝑚 → (𝜑[𝑚 / 𝑏]𝜑))
122121equcoms 2032 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑚 = 𝑏 → (𝜑[𝑚 / 𝑏]𝜑))
123 sbceq1a 3696 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = 𝑛 → ([𝑚 / 𝑏]𝜑[𝑛 / 𝑎][𝑚 / 𝑏]𝜑))
124123equcoms 2032 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = 𝑎 → ([𝑚 / 𝑏]𝜑[𝑛 / 𝑎][𝑚 / 𝑏]𝜑))
125122, 124sylan9bb 513 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑚 = 𝑏𝑛 = 𝑎) → (𝜑[𝑛 / 𝑎][𝑚 / 𝑏]𝜑))
1261253ad2ant2 1135 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑚𝑋𝑛𝑋) ∧ (𝑚 = 𝑏𝑛 = 𝑎) ∧ (𝑥𝑋𝑦𝑋)) → (𝜑[𝑛 / 𝑎][𝑚 / 𝑏]𝜑))
127126biimpa 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑚𝑋𝑛𝑋) ∧ (𝑚 = 𝑏𝑛 = 𝑎) ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝜑) → [𝑛 / 𝑎][𝑚 / 𝑏]𝜑)
128119, 120, 127jca32 519 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑚𝑋𝑛𝑋) ∧ (𝑚 = 𝑏𝑛 = 𝑎) ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝜑) → (((𝑥𝑋𝑦𝑋) ∧ (𝑛𝑋𝑚𝑋)) ∧ (⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩ ∧ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑)))
129 nfv 1921 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑎𝑛, 𝑚⟩ = ⟨𝑛, 𝑚
130 nfsbc1v 3705 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑎[𝑛 / 𝑎][𝑚 / 𝑏]𝜑
131129, 130nfan 1906 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑎(⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩ ∧ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑)
132 nfv 1921 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑏𝑛, 𝑚⟩ = ⟨𝑛, 𝑚
133 nfcv 2900 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑏𝑛
134 nfsbc1v 3705 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑏[𝑚 / 𝑏]𝜑
135133, 134nfsbcw 3707 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑏[𝑛 / 𝑎][𝑚 / 𝑏]𝜑
136132, 135nfan 1906 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩ ∧ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑)
137 opeq12 4773 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑎 = 𝑛𝑏 = 𝑚) → ⟨𝑎, 𝑏⟩ = ⟨𝑛, 𝑚⟩)
138137eqeq2d 2750 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 = 𝑛𝑏 = 𝑚) → (⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩))
139121, 123sylan9bbr 514 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 = 𝑛𝑏 = 𝑚) → (𝜑[𝑛 / 𝑎][𝑚 / 𝑏]𝜑))
140138, 139anbi12d 634 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 = 𝑛𝑏 = 𝑚) → ((⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩ ∧ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑)))
141140adantl 485 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑥𝑋𝑦𝑋) ∧ (𝑎 = 𝑛𝑏 = 𝑚)) → ((⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩ ∧ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑)))
142131, 136, 141spc2ed 3508 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥𝑋𝑦𝑋) ∧ (𝑛𝑋𝑚𝑋)) → ((⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩ ∧ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑) → ∃𝑎𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
143142imp 410 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑥𝑋𝑦𝑋) ∧ (𝑛𝑋𝑚𝑋)) ∧ (⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩ ∧ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑)) → ∃𝑎𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑))
144 pm2.27 42 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑎𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ((∃𝑎𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩))
145128, 143, 1443syl 18 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑚𝑋𝑛𝑋) ∧ (𝑚 = 𝑏𝑛 = 𝑎) ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝜑) → ((∃𝑎𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩))
146 prcom 4633 . . . . . . . . . . . . . . . . . . . . . 22 {𝑛, 𝑚} = {𝑚, 𝑛}
147 oppr 44103 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ V ∧ 𝑚 ∈ V) → (⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩ → {𝑛, 𝑚} = {𝑥, 𝑦}))
148147el2v 3408 . . . . . . . . . . . . . . . . . . . . . 22 (⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩ → {𝑛, 𝑚} = {𝑥, 𝑦})
149146, 148eqtr3id 2788 . . . . . . . . . . . . . . . . . . . . 21 (⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩ → {𝑚, 𝑛} = {𝑥, 𝑦})
150145, 149syl6 35 . . . . . . . . . . . . . . . . . . . 20 ((((𝑚𝑋𝑛𝑋) ∧ (𝑚 = 𝑏𝑛 = 𝑎) ∧ (𝑥𝑋𝑦𝑋)) ∧ 𝜑) → ((∃𝑎𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩) → {𝑚, 𝑛} = {𝑥, 𝑦}))
151150ex 416 . . . . . . . . . . . . . . . . . . 19 (((𝑚𝑋𝑛𝑋) ∧ (𝑚 = 𝑏𝑛 = 𝑎) ∧ (𝑥𝑋𝑦𝑋)) → (𝜑 → ((∃𝑎𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩) → {𝑚, 𝑛} = {𝑥, 𝑦})))
152151com23 86 . . . . . . . . . . . . . . . . . 18 (((𝑚𝑋𝑛𝑋) ∧ (𝑚 = 𝑏𝑛 = 𝑎) ∧ (𝑥𝑋𝑦𝑋)) → ((∃𝑎𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))
1531523exp 1120 . . . . . . . . . . . . . . . . 17 ((𝑚𝑋𝑛𝑋) → ((𝑚 = 𝑏𝑛 = 𝑎) → ((𝑥𝑋𝑦𝑋) → ((∃𝑎𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))))
154153com24 95 . . . . . . . . . . . . . . . 16 ((𝑚𝑋𝑛𝑋) → ((∃𝑎𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩) → ((𝑥𝑋𝑦𝑋) → ((𝑚 = 𝑏𝑛 = 𝑎) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))))
155115, 154syld 47 . . . . . . . . . . . . . . 15 ((𝑚𝑋𝑛𝑋) → (∀𝑖𝑋𝑗𝑋 (∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) → ((𝑥𝑋𝑦𝑋) → ((𝑚 = 𝑏𝑛 = 𝑎) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))))
156155com13 88 . . . . . . . . . . . . . 14 ((𝑥𝑋𝑦𝑋) → (∀𝑖𝑋𝑗𝑋 (∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) → ((𝑚𝑋𝑛𝑋) → ((𝑚 = 𝑏𝑛 = 𝑎) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))))
157156a1d 25 . . . . . . . . . . . . 13 ((𝑥𝑋𝑦𝑋) → (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → (∀𝑖𝑋𝑗𝑋 (∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) → ((𝑚𝑋𝑛𝑋) → ((𝑚 = 𝑏𝑛 = 𝑎) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦}))))))
158157imp42 430 . . . . . . . . . . . 12 ((((𝑥𝑋𝑦𝑋) ∧ (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖𝑋𝑗𝑋 (∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) ∧ (𝑚𝑋𝑛𝑋)) → ((𝑚 = 𝑏𝑛 = 𝑎) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))
159101, 158jaod 858 . . . . . . . . . . 11 ((((𝑥𝑋𝑦𝑋) ∧ (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖𝑋𝑗𝑋 (∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) ∧ (𝑚𝑋𝑛𝑋)) → (((𝑚 = 𝑎𝑛 = 𝑏) ∨ (𝑚 = 𝑏𝑛 = 𝑎)) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))
16048, 159syl5bi 245 . . . . . . . . . 10 ((((𝑥𝑋𝑦𝑋) ∧ (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖𝑋𝑗𝑋 (∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) ∧ (𝑚𝑋𝑛𝑋)) → ({𝑚, 𝑛} = {𝑎, 𝑏} → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))
161160impd 414 . . . . . . . . 9 ((((𝑥𝑋𝑦𝑋) ∧ (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖𝑋𝑗𝑋 (∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) ∧ (𝑚𝑋𝑛𝑋)) → (({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑦}))
16242, 43, 161exlimd 2220 . . . . . . . 8 ((((𝑥𝑋𝑦𝑋) ∧ (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖𝑋𝑗𝑋 (∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) ∧ (𝑚𝑋𝑛𝑋)) → (∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑦}))
16327, 28, 162exlimd 2220 . . . . . . 7 ((((𝑥𝑋𝑦𝑋) ∧ (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖𝑋𝑗𝑋 (∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) ∧ (𝑚𝑋𝑛𝑋)) → (∃𝑎𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑦}))
164163ralrimivva 3104 . . . . . 6 (((𝑥𝑋𝑦𝑋) ∧ (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖𝑋𝑗𝑋 (∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) → ∀𝑚𝑋𝑛𝑋 (∃𝑎𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑦}))
165 preq1 4634 . . . . . . . . . . 11 (𝑣 = 𝑥 → {𝑣, 𝑤} = {𝑥, 𝑤})
166165eqeq1d 2741 . . . . . . . . . 10 (𝑣 = 𝑥 → ({𝑣, 𝑤} = {𝑎, 𝑏} ↔ {𝑥, 𝑤} = {𝑎, 𝑏}))
167166anbi1d 633 . . . . . . . . 9 (𝑣 = 𝑥 → (({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ↔ ({𝑥, 𝑤} = {𝑎, 𝑏} ∧ 𝜑)))
1681672exbidv 1931 . . . . . . . 8 (𝑣 = 𝑥 → (∃𝑎𝑏({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ↔ ∃𝑎𝑏({𝑥, 𝑤} = {𝑎, 𝑏} ∧ 𝜑)))
169165eqeq2d 2750 . . . . . . . . . 10 (𝑣 = 𝑥 → ({𝑚, 𝑛} = {𝑣, 𝑤} ↔ {𝑚, 𝑛} = {𝑥, 𝑤}))
170169imbi2d 344 . . . . . . . . 9 (𝑣 = 𝑥 → ((∃𝑎𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑣, 𝑤}) ↔ (∃𝑎𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑤})))
1711702ralbidv 3112 . . . . . . . 8 (𝑣 = 𝑥 → (∀𝑚𝑋𝑛𝑋 (∃𝑎𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑣, 𝑤}) ↔ ∀𝑚𝑋𝑛𝑋 (∃𝑎𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑤})))
172168, 171anbi12d 634 . . . . . . 7 (𝑣 = 𝑥 → ((∃𝑎𝑏({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚𝑋𝑛𝑋 (∃𝑎𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑣, 𝑤})) ↔ (∃𝑎𝑏({𝑥, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚𝑋𝑛𝑋 (∃𝑎𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑤}))))
173 preq2 4635 . . . . . . . . . . 11 (𝑤 = 𝑦 → {𝑥, 𝑤} = {𝑥, 𝑦})
174173eqeq1d 2741 . . . . . . . . . 10 (𝑤 = 𝑦 → ({𝑥, 𝑤} = {𝑎, 𝑏} ↔ {𝑥, 𝑦} = {𝑎, 𝑏}))
175174anbi1d 633 . . . . . . . . 9 (𝑤 = 𝑦 → (({𝑥, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ↔ ({𝑥, 𝑦} = {𝑎, 𝑏} ∧ 𝜑)))
1761752exbidv 1931 . . . . . . . 8 (𝑤 = 𝑦 → (∃𝑎𝑏({𝑥, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ↔ ∃𝑎𝑏({𝑥, 𝑦} = {𝑎, 𝑏} ∧ 𝜑)))
177173eqeq2d 2750 . . . . . . . . . 10 (𝑤 = 𝑦 → ({𝑚, 𝑛} = {𝑥, 𝑤} ↔ {𝑚, 𝑛} = {𝑥, 𝑦}))
178177imbi2d 344 . . . . . . . . 9 (𝑤 = 𝑦 → ((∃𝑎𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑤}) ↔ (∃𝑎𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑦})))
1791782ralbidv 3112 . . . . . . . 8 (𝑤 = 𝑦 → (∀𝑚𝑋𝑛𝑋 (∃𝑎𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑤}) ↔ ∀𝑚𝑋𝑛𝑋 (∃𝑎𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑦})))
180176, 179anbi12d 634 . . . . . . 7 (𝑤 = 𝑦 → ((∃𝑎𝑏({𝑥, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚𝑋𝑛𝑋 (∃𝑎𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑤})) ↔ (∃𝑎𝑏({𝑥, 𝑦} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚𝑋𝑛𝑋 (∃𝑎𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑦}))))
181172, 180rspc2ev 3541 . . . . . 6 ((𝑥𝑋𝑦𝑋 ∧ (∃𝑎𝑏({𝑥, 𝑦} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚𝑋𝑛𝑋 (∃𝑎𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑦}))) → ∃𝑣𝑋𝑤𝑋 (∃𝑎𝑏({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚𝑋𝑛𝑋 (∃𝑎𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑣, 𝑤})))
1828, 9, 15, 164, 181syl112anc 1375 . . . . 5 (((𝑥𝑋𝑦𝑋) ∧ (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖𝑋𝑗𝑋 (∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) → ∃𝑣𝑋𝑤𝑋 (∃𝑎𝑏({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚𝑋𝑛𝑋 (∃𝑎𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑣, 𝑤})))
183182ex 416 . . . 4 ((𝑥𝑋𝑦𝑋) → ((∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖𝑋𝑗𝑋 (∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)) → ∃𝑣𝑋𝑤𝑋 (∃𝑎𝑏({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚𝑋𝑛𝑋 (∃𝑎𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑣, 𝑤}))))
184183rexlimivv 3203 . . 3 (∃𝑥𝑋𝑦𝑋 (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖𝑋𝑗𝑋 (∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)) → ∃𝑣𝑋𝑤𝑋 (∃𝑎𝑏({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚𝑋𝑛𝑋 (∃𝑎𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑣, 𝑤})))
185 eqeq1 2743 . . . . . 6 (𝑝 = {𝑣, 𝑤} → (𝑝 = {𝑎, 𝑏} ↔ {𝑣, 𝑤} = {𝑎, 𝑏}))
186185anbi1d 633 . . . . 5 (𝑝 = {𝑣, 𝑤} → ((𝑝 = {𝑎, 𝑏} ∧ 𝜑) ↔ ({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑)))
1871862exbidv 1931 . . . 4 (𝑝 = {𝑣, 𝑤} → (∃𝑎𝑏(𝑝 = {𝑎, 𝑏} ∧ 𝜑) ↔ ∃𝑎𝑏({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑)))
188 eqeq1 2743 . . . . . 6 (𝑝 = {𝑚, 𝑛} → (𝑝 = {𝑎, 𝑏} ↔ {𝑚, 𝑛} = {𝑎, 𝑏}))
189188anbi1d 633 . . . . 5 (𝑝 = {𝑚, 𝑛} → ((𝑝 = {𝑎, 𝑏} ∧ 𝜑) ↔ ({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑)))
1901892exbidv 1931 . . . 4 (𝑝 = {𝑚, 𝑛} → (∃𝑎𝑏(𝑝 = {𝑎, 𝑏} ∧ 𝜑) ↔ ∃𝑎𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑)))
191187, 190reupr 44555 . . 3 (𝑋𝑉 → (∃!𝑝 ∈ (Pairs‘𝑋)∃𝑎𝑏(𝑝 = {𝑎, 𝑏} ∧ 𝜑) ↔ ∃𝑣𝑋𝑤𝑋 (∃𝑎𝑏({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚𝑋𝑛𝑋 (∃𝑎𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑣, 𝑤}))))
192184, 191syl5ibr 249 . 2 (𝑋𝑉 → (∃𝑥𝑋𝑦𝑋 (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖𝑋𝑗𝑋 (∃𝑎𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)) → ∃!𝑝 ∈ (Pairs‘𝑋)∃𝑎𝑏(𝑝 = {𝑎, 𝑏} ∧ 𝜑)))
1937, 192syl5bi 245 1 (𝑋𝑉 → (∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ∃!𝑝 ∈ (Pairs‘𝑋)∃𝑎𝑏(𝑝 = {𝑎, 𝑏} ∧ 𝜑)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wo 846  w3a 1088   = wceq 1542  wex 1786  wcel 2114  wral 3054  wrex 3055  ∃!wreu 3056  Vcvv 3400  [wsbc 3685  {cpr 4528  cop 4532   × cxp 5533  cfv 6349  Pairscspr 44510
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2711  ax-rep 5164  ax-sep 5177  ax-nul 5184  ax-pr 5306  ax-un 7491
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2541  df-eu 2571  df-clab 2718  df-cleq 2731  df-clel 2812  df-nfc 2882  df-ne 2936  df-ral 3059  df-rex 3060  df-reu 3061  df-rab 3063  df-v 3402  df-sbc 3686  df-csb 3801  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4222  df-if 4425  df-pw 4500  df-sn 4527  df-pr 4529  df-op 4533  df-uni 4807  df-iun 4893  df-br 5041  df-opab 5103  df-mpt 5121  df-id 5439  df-xp 5541  df-rel 5542  df-cnv 5543  df-co 5544  df-dm 5545  df-rn 5546  df-res 5547  df-ima 5548  df-iota 6307  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-spr 44511
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator