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 44978
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 2742 . . . . 5 (𝑝 = ⟨𝑥, 𝑦⟩ → (𝑝 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))
21anbi1d 630 . . . 4 (𝑝 = ⟨𝑥, 𝑦⟩ → ((𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
322exbidv 1927 . . 3 (𝑝 = ⟨𝑥, 𝑦⟩ → (∃𝑎∃𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
4 eqeq1 2742 . . . . 5 (𝑝 = ⟨𝑖, 𝑗⟩ → (𝑝 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩))
54anbi1d 630 . . . 4 (𝑝 = ⟨𝑖, 𝑗⟩ → ((𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
652exbidv 1927 . . 3 (𝑝 = ⟨𝑖, 𝑗⟩ → (∃𝑎∃𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
73, 6reuop 6196 . 2 (∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎∃𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)))
8 simpll 764 . . . . . 6 (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) → 𝑥 ∈ 𝑋)
9 simplr 766 . . . . . 6 (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) → 𝑦 ∈ 𝑋)
10 oppr 44524 . . . . . . . . . . 11 ((𝑥 ∈ V ∧ 𝑦 ∈ V) → (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ → {𝑥, 𝑦} = {𝑎, 𝑏}))
1110el2v 3440 . . . . . . . . . 10 (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ → {𝑥, 𝑦} = {𝑎, 𝑏})
1211anim1i 615 . . . . . . . . 9 ((⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ({𝑥, 𝑦} = {𝑎, 𝑏} ∧ 𝜑))
13122eximi 1838 . . . . . . . 8 (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ∃𝑎∃𝑏({𝑥, 𝑦} = {𝑎, 𝑏} ∧ 𝜑))
1413adantr 481 . . . . . . 7 ((∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)) → ∃𝑎∃𝑏({𝑥, 𝑦} = {𝑎, 𝑏} ∧ 𝜑))
1514adantl 482 . . . . . 6 (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) → ∃𝑎∃𝑏({𝑥, 𝑦} = {𝑎, 𝑏} ∧ 𝜑))
16 nfv 1917 . . . . . . . . . 10 Ⅎ𝑎(𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)
17 nfe1 2147 . . . . . . . . . . 11 Ⅎ𝑎∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)
18 nfcv 2907 . . . . . . . . . . . 12 Ⅎ𝑎𝑋
19 nfe1 2147 . . . . . . . . . . . . . 14 Ⅎ𝑎∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)
20 nfv 1917 . . . . . . . . . . . . . 14 Ⅎ𝑎⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩
2119, 20nfim 1899 . . . . . . . . . . . . 13 Ⅎ𝑎(∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)
2218, 21nfralw 3151 . . . . . . . . . . . 12 Ⅎ𝑎∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)
2318, 22nfralw 3151 . . . . . . . . . . 11 Ⅎ𝑎∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)
2417, 23nfan 1902 . . . . . . . . . 10 Ⅎ𝑎(∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))
2516, 24nfan 1902 . . . . . . . . 9 Ⅎ𝑎((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)))
26 nfv 1917 . . . . . . . . 9 Ⅎ𝑎(𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)
2725, 26nfan 1902 . . . . . . . 8 Ⅎ𝑎(((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋))
28 nfv 1917 . . . . . . . 8 Ⅎ𝑎{𝑚, 𝑛} = {𝑥, 𝑦}
29 nfv 1917 . . . . . . . . . . 11 Ⅎ𝑏(𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)
30 nfe1 2147 . . . . . . . . . . . . 13 Ⅎ𝑏∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)
3130nfex 2318 . . . . . . . . . . . 12 Ⅎ𝑏∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)
32 nfcv 2907 . . . . . . . . . . . . 13 Ⅎ𝑏𝑋
33 nfe1 2147 . . . . . . . . . . . . . . . 16 Ⅎ𝑏∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)
3433nfex 2318 . . . . . . . . . . . . . . 15 Ⅎ𝑏∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)
35 nfv 1917 . . . . . . . . . . . . . . 15 Ⅎ𝑏⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩
3634, 35nfim 1899 . . . . . . . . . . . . . 14 Ⅎ𝑏(∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)
3732, 36nfralw 3151 . . . . . . . . . . . . 13 Ⅎ𝑏∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)
3832, 37nfralw 3151 . . . . . . . . . . . 12 Ⅎ𝑏∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)
3931, 38nfan 1902 . . . . . . . . . . 11 Ⅎ𝑏(∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))
4029, 39nfan 1902 . . . . . . . . . 10 Ⅎ𝑏((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)))
41 nfv 1917 . . . . . . . . . 10 Ⅎ𝑏(𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)
4240, 41nfan 1902 . . . . . . . . 9 Ⅎ𝑏(((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋))
43 nfv 1917 . . . . . . . . 9 Ⅎ𝑏{𝑚, 𝑛} = {𝑥, 𝑦}
44 vex 3436 . . . . . . . . . . . 12 𝑚 ∈ V
45 vex 3436 . . . . . . . . . . . 12 𝑛 ∈ V
46 vex 3436 . . . . . . . . . . . 12 𝑎 ∈ V
47 vex 3436 . . . . . . . . . . . 12 𝑏 ∈ V
4844, 45, 46, 47preq12b 4781 . . . . . . . . . . 11 ({𝑚, 𝑛} = {𝑎, 𝑏} ↔ ((𝑚 = 𝑎 ∧ 𝑛 = 𝑏) ∨ (𝑚 = 𝑏 ∧ 𝑛 = 𝑎)))
49 opeq1 4804 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 𝑚 → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑗⟩)
5049eqeq1d 2740 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑚 → (⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑚, 𝑗⟩ = ⟨𝑎, 𝑏⟩))
5150anbi1d 630 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑚 → ((⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑚, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
52512exbidv 1927 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑚 → (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑎∃𝑏(⟨𝑚, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
5349eqeq1d 2740 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑚 → (⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑚, 𝑗⟩ = ⟨𝑥, 𝑦⟩))
5452, 53imbi12d 345 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑚 → ((∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) ↔ (∃𝑎∃𝑏(⟨𝑚, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑗⟩ = ⟨𝑥, 𝑦⟩)))
55 opeq2 4805 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑛 → ⟨𝑚, 𝑗⟩ = ⟨𝑚, 𝑛⟩)
5655eqeq1d 2740 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑛 → (⟨𝑚, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩))
5756anbi1d 630 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑛 → ((⟨𝑚, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
58572exbidv 1927 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑛 → (∃𝑎∃𝑏(⟨𝑚, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
5955eqeq1d 2740 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑛 → (⟨𝑚, 𝑗⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩))
6058, 59imbi12d 345 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑛 → ((∃𝑎∃𝑏(⟨𝑚, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑗⟩ = ⟨𝑥, 𝑦⟩) ↔ (∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩)))
6154, 60rspc2v 3570 . . . . . . . . . . . . . . . 16 ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → (∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) → (∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩)))
62 pm3.22 460 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)))
63623adant2 1130 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑎 ∧ 𝑛 = 𝑏) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)))
6463adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑎 ∧ 𝑛 = 𝑏) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝜑) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)))
65 eqidd 2739 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑎 ∧ 𝑛 = 𝑏) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩)
66 sbceq1a 3727 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = 𝑚 → (𝜑 ↔ [𝑚 / 𝑎]𝜑))
6766equcoms 2023 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑚 = 𝑎 → (𝜑 ↔ [𝑚 / 𝑎]𝜑))
68 sbceq1a 3727 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 = 𝑛 → ([𝑚 / 𝑎]𝜑 ↔ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑))
6968equcoms 2023 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = 𝑏 → ([𝑚 / 𝑎]𝜑 ↔ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑))
7067, 69sylan9bb 510 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑚 = 𝑎 ∧ 𝑛 = 𝑏) → (𝜑 ↔ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑))
71703ad2ant2 1133 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑎 ∧ 𝑛 = 𝑏) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝜑 ↔ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑))
7271biimpa 477 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑎 ∧ 𝑛 = 𝑏) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝜑) → [𝑛 / 𝑏][𝑚 / 𝑎]𝜑)
7364, 65, 72jca32 516 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑎 ∧ 𝑛 = 𝑏) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝜑) → (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)) ∧ (⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩ ∧ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑)))
74 nfv 1917 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ⅎ𝑎⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩
75 nfcv 2907 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Ⅎ𝑎𝑛
76 nfsbc1v 3736 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Ⅎ𝑎[𝑚 / 𝑎]𝜑
7775, 76nfsbcw 3738 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ⅎ𝑎[𝑛 / 𝑏][𝑚 / 𝑎]𝜑
7874, 77nfan 1902 . . . . . . . . . . . . . . . . . . . . . . . 24 Ⅎ𝑎(⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩ ∧ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑)
79 nfv 1917 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ⅎ𝑏⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩
80 nfsbc1v 3736 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ⅎ𝑏[𝑛 / 𝑏][𝑚 / 𝑎]𝜑
8179, 80nfan 1902 . . . . . . . . . . . . . . . . . . . . . . . 24 Ⅎ𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩ ∧ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑)
82 opeq12 4806 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑎 = 𝑚 ∧ 𝑏 = 𝑛) → ⟨𝑎, 𝑏⟩ = ⟨𝑚, 𝑛⟩)
8382eqeq2d 2749 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 = 𝑚 ∧ 𝑏 = 𝑛) → (⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩))
8466, 68sylan9bb 510 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 = 𝑚 ∧ 𝑏 = 𝑛) → (𝜑 ↔ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑))
8583, 84anbi12d 631 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 = 𝑚 ∧ 𝑏 = 𝑛) → ((⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩ ∧ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑)))
8685adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑎 = 𝑚 ∧ 𝑏 = 𝑛)) → ((⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩ ∧ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑)))
8778, 81, 86spc2ed 3540 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)) → ((⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩ ∧ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑) → ∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
8887imp 407 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)) ∧ (⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩ ∧ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑)) → ∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑))
89 pm2.27 42 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ((∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩))
9073, 88, 893syl 18 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑎 ∧ 𝑛 = 𝑏) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝜑) → ((∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩))
91 oppr 44524 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑚 ∈ V ∧ 𝑛 ∈ V) → (⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩ → {𝑚, 𝑛} = {𝑥, 𝑦}))
9291el2v 3440 . . . . . . . . . . . . . . . . . . . . 21 (⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩ → {𝑚, 𝑛} = {𝑥, 𝑦})
9390, 92syl6 35 . . . . . . . . . . . . . . . . . . . 20 ((((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑎 ∧ 𝑛 = 𝑏) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝜑) → ((∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩) → {𝑚, 𝑛} = {𝑥, 𝑦}))
9493ex 413 . . . . . . . . . . . . . . . . . . 19 (((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑎 ∧ 𝑛 = 𝑏) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝜑 → ((∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩) → {𝑚, 𝑛} = {𝑥, 𝑦})))
9594com23 86 . . . . . . . . . . . . . . . . . 18 (((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑎 ∧ 𝑛 = 𝑏) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))
96953exp 1118 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → ((𝑚 = 𝑎 ∧ 𝑛 = 𝑏) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))))
9796com24 95 . . . . . . . . . . . . . . . 16 ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → ((∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑚 = 𝑎 ∧ 𝑛 = 𝑏) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))))
9861, 97syld 47 . . . . . . . . . . . . . . 15 ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → (∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑚 = 𝑎 ∧ 𝑛 = 𝑏) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))))
9998com13 88 . . . . . . . . . . . . . 14 ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) → ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → ((𝑚 = 𝑎 ∧ 𝑛 = 𝑏) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))))
10099a1d 25 . . . . . . . . . . . . 13 ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → (∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) → ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → ((𝑚 = 𝑎 ∧ 𝑛 = 𝑏) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦}))))))
101100imp42 427 . . . . . . . . . . . 12 ((((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)) → ((𝑚 = 𝑎 ∧ 𝑛 = 𝑏) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))
102 opeq1 4804 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = 𝑛 → ⟨𝑖, 𝑗⟩ = ⟨𝑛, 𝑗⟩)
103102eqeq1d 2740 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 𝑛 → (⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑛, 𝑗⟩ = ⟨𝑎, 𝑏⟩))
104103anbi1d 630 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑛 → ((⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑛, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
1051042exbidv 1927 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑛 → (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑎∃𝑏(⟨𝑛, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
106102eqeq1d 2740 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑛 → (⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑛, 𝑗⟩ = ⟨𝑥, 𝑦⟩))
107105, 106imbi12d 345 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑛 → ((∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) ↔ (∃𝑎∃𝑏(⟨𝑛, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑗⟩ = ⟨𝑥, 𝑦⟩)))
108 opeq2 4805 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑚 → ⟨𝑛, 𝑗⟩ = ⟨𝑛, 𝑚⟩)
109108eqeq1d 2740 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑚 → (⟨𝑛, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩))
110109anbi1d 630 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑚 → ((⟨𝑛, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
1111102exbidv 1927 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑚 → (∃𝑎∃𝑏(⟨𝑛, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
112108eqeq1d 2740 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑚 → (⟨𝑛, 𝑗⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩))
113111, 112imbi12d 345 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑚 → ((∃𝑎∃𝑏(⟨𝑛, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑗⟩ = ⟨𝑥, 𝑦⟩) ↔ (∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩)))
114107, 113rspc2v 3570 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ 𝑋 ∧ 𝑚 ∈ 𝑋) → (∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) → (∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩)))
115114ancoms 459 . . . . . . . . . . . . . . . 16 ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → (∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) → (∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩)))
116 pm3.22 460 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → (𝑛 ∈ 𝑋 ∧ 𝑚 ∈ 𝑋))
117116anim1ci 616 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑛 ∈ 𝑋 ∧ 𝑚 ∈ 𝑋)))
1181173adant2 1130 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑏 ∧ 𝑛 = 𝑎) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑛 ∈ 𝑋 ∧ 𝑚 ∈ 𝑋)))
119118adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑏 ∧ 𝑛 = 𝑎) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝜑) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑛 ∈ 𝑋 ∧ 𝑚 ∈ 𝑋)))
120 eqidd 2739 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑏 ∧ 𝑛 = 𝑎) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩)
121 sbceq1a 3727 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 = 𝑚 → (𝜑 ↔ [𝑚 / 𝑏]𝜑))
122121equcoms 2023 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑚 = 𝑏 → (𝜑 ↔ [𝑚 / 𝑏]𝜑))
123 sbceq1a 3727 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = 𝑛 → ([𝑚 / 𝑏]𝜑 ↔ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑))
124123equcoms 2023 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = 𝑎 → ([𝑚 / 𝑏]𝜑 ↔ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑))
125122, 124sylan9bb 510 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑚 = 𝑏 ∧ 𝑛 = 𝑎) → (𝜑 ↔ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑))
1261253ad2ant2 1133 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑏 ∧ 𝑛 = 𝑎) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝜑 ↔ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑))
127126biimpa 477 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑏 ∧ 𝑛 = 𝑎) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝜑) → [𝑛 / 𝑎][𝑚 / 𝑏]𝜑)
128119, 120, 127jca32 516 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑏 ∧ 𝑛 = 𝑎) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝜑) → (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑛 ∈ 𝑋 ∧ 𝑚 ∈ 𝑋)) ∧ (⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩ ∧ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑)))
129 nfv 1917 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ⅎ𝑎⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩
130 nfsbc1v 3736 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ⅎ𝑎[𝑛 / 𝑎][𝑚 / 𝑏]𝜑
131129, 130nfan 1902 . . . . . . . . . . . . . . . . . . . . . . . 24 Ⅎ𝑎(⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩ ∧ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑)
132 nfv 1917 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ⅎ𝑏⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩
133 nfcv 2907 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Ⅎ𝑏𝑛
134 nfsbc1v 3736 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Ⅎ𝑏[𝑚 / 𝑏]𝜑
135133, 134nfsbcw 3738 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ⅎ𝑏[𝑛 / 𝑎][𝑚 / 𝑏]𝜑
136132, 135nfan 1902 . . . . . . . . . . . . . . . . . . . . . . . 24 Ⅎ𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩ ∧ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑)
137 opeq12 4806 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑎 = 𝑛 ∧ 𝑏 = 𝑚) → ⟨𝑎, 𝑏⟩ = ⟨𝑛, 𝑚⟩)
138137eqeq2d 2749 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 = 𝑛 ∧ 𝑏 = 𝑚) → (⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩))
139121, 123sylan9bbr 511 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 = 𝑛 ∧ 𝑏 = 𝑚) → (𝜑 ↔ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑))
140138, 139anbi12d 631 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 = 𝑛 ∧ 𝑏 = 𝑚) → ((⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩ ∧ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑)))
141140adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑎 = 𝑛 ∧ 𝑏 = 𝑚)) → ((⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩ ∧ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑)))
142131, 136, 141spc2ed 3540 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑛 ∈ 𝑋 ∧ 𝑚 ∈ 𝑋)) → ((⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩ ∧ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑) → ∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
143142imp 407 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑛 ∈ 𝑋 ∧ 𝑚 ∈ 𝑋)) ∧ (⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩ ∧ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑)) → ∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑))
144 pm2.27 42 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ((∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩))
145128, 143, 1443syl 18 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑏 ∧ 𝑛 = 𝑎) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝜑) → ((∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩))
146 prcom 4668 . . . . . . . . . . . . . . . . . . . . . 22 {𝑛, 𝑚} = {𝑚, 𝑛}
147 oppr 44524 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ V ∧ 𝑚 ∈ V) → (⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩ → {𝑛, 𝑚} = {𝑥, 𝑦}))
148147el2v 3440 . . . . . . . . . . . . . . . . . . . . . 22 (⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩ → {𝑛, 𝑚} = {𝑥, 𝑦})
149146, 148eqtr3id 2792 . . . . . . . . . . . . . . . . . . . . 21 (⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩ → {𝑚, 𝑛} = {𝑥, 𝑦})
150145, 149syl6 35 . . . . . . . . . . . . . . . . . . . 20 ((((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑏 ∧ 𝑛 = 𝑎) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝜑) → ((∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩) → {𝑚, 𝑛} = {𝑥, 𝑦}))
151150ex 413 . . . . . . . . . . . . . . . . . . 19 (((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑏 ∧ 𝑛 = 𝑎) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝜑 → ((∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩) → {𝑚, 𝑛} = {𝑥, 𝑦})))
152151com23 86 . . . . . . . . . . . . . . . . . 18 (((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑏 ∧ 𝑛 = 𝑎) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))
1531523exp 1118 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → ((𝑚 = 𝑏 ∧ 𝑛 = 𝑎) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))))
154153com24 95 . . . . . . . . . . . . . . . 16 ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → ((∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑚 = 𝑏 ∧ 𝑛 = 𝑎) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))))
155115, 154syld 47 . . . . . . . . . . . . . . 15 ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → (∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑚 = 𝑏 ∧ 𝑛 = 𝑎) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))))
156155com13 88 . . . . . . . . . . . . . 14 ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) → ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → ((𝑚 = 𝑏 ∧ 𝑛 = 𝑎) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))))
157156a1d 25 . . . . . . . . . . . . 13 ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → (∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) → ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → ((𝑚 = 𝑏 ∧ 𝑛 = 𝑎) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦}))))))
158157imp42 427 . . . . . . . . . . . 12 ((((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)) → ((𝑚 = 𝑏 ∧ 𝑛 = 𝑎) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))
159101, 158jaod 856 . . . . . . . . . . 11 ((((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)) → (((𝑚 = 𝑎 ∧ 𝑛 = 𝑏) ∨ (𝑚 = 𝑏 ∧ 𝑛 = 𝑎)) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))
16048, 159syl5bi 241 . . . . . . . . . 10 ((((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)) → ({𝑚, 𝑛} = {𝑎, 𝑏} → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))
161160impd 411 . . . . . . . . 9 ((((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)) → (({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑦}))
16242, 43, 161exlimd 2211 . . . . . . . 8 ((((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)) → (∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑦}))
16327, 28, 162exlimd 2211 . . . . . . 7 ((((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)) → (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑦}))
164163ralrimivva 3123 . . . . . 6 (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) → ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑦}))
165 preq1 4669 . . . . . . . . . . 11 (𝑣 = 𝑥 → {𝑣, 𝑤} = {𝑥, 𝑤})
166165eqeq1d 2740 . . . . . . . . . 10 (𝑣 = 𝑥 → ({𝑣, 𝑤} = {𝑎, 𝑏} ↔ {𝑥, 𝑤} = {𝑎, 𝑏}))
167166anbi1d 630 . . . . . . . . 9 (𝑣 = 𝑥 → (({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ↔ ({𝑥, 𝑤} = {𝑎, 𝑏} ∧ 𝜑)))
1681672exbidv 1927 . . . . . . . 8 (𝑣 = 𝑥 → (∃𝑎∃𝑏({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ↔ ∃𝑎∃𝑏({𝑥, 𝑤} = {𝑎, 𝑏} ∧ 𝜑)))
169165eqeq2d 2749 . . . . . . . . . 10 (𝑣 = 𝑥 → ({𝑚, 𝑛} = {𝑣, 𝑤} ↔ {𝑚, 𝑛} = {𝑥, 𝑤}))
170169imbi2d 341 . . . . . . . . 9 (𝑣 = 𝑥 → ((∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑣, 𝑤}) ↔ (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑤})))
1711702ralbidv 3129 . . . . . . . 8 (𝑣 = 𝑥 → (∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑣, 𝑤}) ↔ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑤})))
172168, 171anbi12d 631 . . . . . . 7 (𝑣 = 𝑥 → ((∃𝑎∃𝑏({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑣, 𝑤})) ↔ (∃𝑎∃𝑏({𝑥, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑤}))))
173 preq2 4670 . . . . . . . . . . 11 (𝑤 = 𝑦 → {𝑥, 𝑤} = {𝑥, 𝑦})
174173eqeq1d 2740 . . . . . . . . . 10 (𝑤 = 𝑦 → ({𝑥, 𝑤} = {𝑎, 𝑏} ↔ {𝑥, 𝑦} = {𝑎, 𝑏}))
175174anbi1d 630 . . . . . . . . 9 (𝑤 = 𝑦 → (({𝑥, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ↔ ({𝑥, 𝑦} = {𝑎, 𝑏} ∧ 𝜑)))
1761752exbidv 1927 . . . . . . . 8 (𝑤 = 𝑦 → (∃𝑎∃𝑏({𝑥, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ↔ ∃𝑎∃𝑏({𝑥, 𝑦} = {𝑎, 𝑏} ∧ 𝜑)))
177173eqeq2d 2749 . . . . . . . . . 10 (𝑤 = 𝑦 → ({𝑚, 𝑛} = {𝑥, 𝑤} ↔ {𝑚, 𝑛} = {𝑥, 𝑦}))
178177imbi2d 341 . . . . . . . . 9 (𝑤 = 𝑦 → ((∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑤}) ↔ (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑦})))
1791782ralbidv 3129 . . . . . . . 8 (𝑤 = 𝑦 → (∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑤}) ↔ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑦})))
180176, 179anbi12d 631 . . . . . . 7 (𝑤 = 𝑦 → ((∃𝑎∃𝑏({𝑥, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑤})) ↔ (∃𝑎∃𝑏({𝑥, 𝑦} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑦}))))
181172, 180rspc2ev 3572 . . . . . 6 ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (∃𝑎∃𝑏({𝑥, 𝑦} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑦}))) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑋 (∃𝑎∃𝑏({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑣, 𝑤})))
1828, 9, 15, 164, 181syl112anc 1373 . . . . 5 (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑋 (∃𝑎∃𝑏({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑣, 𝑤})))
183182ex 413 . . . 4 ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑋 (∃𝑎∃𝑏({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑣, 𝑤}))))
184183rexlimivv 3221 . . 3 (∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑋 (∃𝑎∃𝑏({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑣, 𝑤})))
185 eqeq1 2742 . . . . . 6 (𝑝 = {𝑣, 𝑤} → (𝑝 = {𝑎, 𝑏} ↔ {𝑣, 𝑤} = {𝑎, 𝑏}))
186185anbi1d 630 . . . . 5 (𝑝 = {𝑣, 𝑤} → ((𝑝 = {𝑎, 𝑏} ∧ 𝜑) ↔ ({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑)))
1871862exbidv 1927 . . . 4 (𝑝 = {𝑣, 𝑤} → (∃𝑎∃𝑏(𝑝 = {𝑎, 𝑏} ∧ 𝜑) ↔ ∃𝑎∃𝑏({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑)))
188 eqeq1 2742 . . . . . 6 (𝑝 = {𝑚, 𝑛} → (𝑝 = {𝑎, 𝑏} ↔ {𝑚, 𝑛} = {𝑎, 𝑏}))
189188anbi1d 630 . . . . 5 (𝑝 = {𝑚, 𝑛} → ((𝑝 = {𝑎, 𝑏} ∧ 𝜑) ↔ ({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑)))
1901892exbidv 1927 . . . 4 (𝑝 = {𝑚, 𝑛} → (∃𝑎∃𝑏(𝑝 = {𝑎, 𝑏} ∧ 𝜑) ↔ ∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑)))
191187, 190reupr 44974 . . 3 (𝑋 ∈ 𝑉 → (∃!𝑝 ∈ (Pairs‘𝑋)∃𝑎∃𝑏(𝑝 = {𝑎, 𝑏} ∧ 𝜑) ↔ ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑋 (∃𝑎∃𝑏({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑣, 𝑤}))))
192184, 191syl5ibr 245 . 2 (𝑋 ∈ 𝑉 → (∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)) → ∃!𝑝 ∈ (Pairs‘𝑋)∃𝑎∃𝑏(𝑝 = {𝑎, 𝑏} ∧ 𝜑)))
1937, 192syl5bi 241 1 (𝑋 ∈ 𝑉 → (∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎∃𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ∃!𝑝 ∈ (Pairs‘𝑋)∃𝑎∃𝑏(𝑝 = {𝑎, 𝑏} ∧ 𝜑)))
Colors of variables: wff setvar class
Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 844   ∧ w3a 1086   = wceq 1539  ∃wex 1782   ∈ wcel 2106  ∀wral 3064  ∃wrex 3065  ∃!wreu 3066  Vcvv 3432  [wsbc 3716  {cpr 4563  ⟨cop 4567   × cxp 5587  ‘cfv 6433  Pairscspr 44929
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-un 7588
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-iota 6391  df-fun 6435  df-fv 6441  df-spr 44930
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator