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 43184
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 2798 . . . . 5 (𝑝 = ⟨𝑥, 𝑦⟩ → (𝑝 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))
21anbi1d 629 . . . 4 (𝑝 = ⟨𝑥, 𝑦⟩ → ((𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
322exbidv 1903 . . 3 (𝑝 = ⟨𝑥, 𝑦⟩ → (∃𝑎∃𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
4 eqeq1 2798 . . . . 5 (𝑝 = ⟨𝑖, 𝑗⟩ → (𝑝 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩))
54anbi1d 629 . . . 4 (𝑝 = ⟨𝑖, 𝑗⟩ → ((𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
652exbidv 1903 . . 3 (𝑝 = ⟨𝑖, 𝑗⟩ → (∃𝑎∃𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
73, 6reuop 6022 . 2 (∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎∃𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)))
8 simpll 763 . . . . . 6 (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) → 𝑥 ∈ 𝑋)
9 simplr 765 . . . . . 6 (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) → 𝑦 ∈ 𝑋)
10 oppr 42795 . . . . . . . . . . 11 ((𝑥 ∈ V ∧ 𝑦 ∈ V) → (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ → {𝑥, 𝑦} = {𝑎, 𝑏}))
1110el2v 3443 . . . . . . . . . 10 (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ → {𝑥, 𝑦} = {𝑎, 𝑏})
1211anim1i 614 . . . . . . . . 9 ((⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ({𝑥, 𝑦} = {𝑎, 𝑏} ∧ 𝜑))
13122eximi 1818 . . . . . . . 8 (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ∃𝑎∃𝑏({𝑥, 𝑦} = {𝑎, 𝑏} ∧ 𝜑))
1413adantr 481 . . . . . . 7 ((∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)) → ∃𝑎∃𝑏({𝑥, 𝑦} = {𝑎, 𝑏} ∧ 𝜑))
1514adantl 482 . . . . . 6 (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) → ∃𝑎∃𝑏({𝑥, 𝑦} = {𝑎, 𝑏} ∧ 𝜑))
16 nfv 1893 . . . . . . . . . 10 Ⅎ𝑎(𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)
17 nfe1 2119 . . . . . . . . . . 11 Ⅎ𝑎∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)
18 nfcv 2948 . . . . . . . . . . . 12 Ⅎ𝑎𝑋
19 nfe1 2119 . . . . . . . . . . . . . 14 Ⅎ𝑎∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)
20 nfv 1893 . . . . . . . . . . . . . 14 Ⅎ𝑎⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩
2119, 20nfim 1879 . . . . . . . . . . . . 13 Ⅎ𝑎(∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)
2218, 21nfral 3190 . . . . . . . . . . . 12 Ⅎ𝑎∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)
2318, 22nfral 3190 . . . . . . . . . . 11 Ⅎ𝑎∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)
2417, 23nfan 1882 . . . . . . . . . 10 Ⅎ𝑎(∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))
2516, 24nfan 1882 . . . . . . . . 9 Ⅎ𝑎((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)))
26 nfv 1893 . . . . . . . . 9 Ⅎ𝑎(𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)
2725, 26nfan 1882 . . . . . . . 8 Ⅎ𝑎(((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋))
28 nfv 1893 . . . . . . . 8 Ⅎ𝑎{𝑚, 𝑛} = {𝑥, 𝑦}
29 nfv 1893 . . . . . . . . . . 11 Ⅎ𝑏(𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)
30 nfe1 2119 . . . . . . . . . . . . 13 Ⅎ𝑏∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)
3130nfex 2305 . . . . . . . . . . . 12 Ⅎ𝑏∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)
32 nfcv 2948 . . . . . . . . . . . . 13 Ⅎ𝑏𝑋
33 nfe1 2119 . . . . . . . . . . . . . . . 16 Ⅎ𝑏∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)
3433nfex 2305 . . . . . . . . . . . . . . 15 Ⅎ𝑏∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)
35 nfv 1893 . . . . . . . . . . . . . . 15 Ⅎ𝑏⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩
3634, 35nfim 1879 . . . . . . . . . . . . . 14 Ⅎ𝑏(∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)
3732, 36nfral 3190 . . . . . . . . . . . . 13 Ⅎ𝑏∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)
3832, 37nfral 3190 . . . . . . . . . . . 12 Ⅎ𝑏∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)
3931, 38nfan 1882 . . . . . . . . . . 11 Ⅎ𝑏(∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))
4029, 39nfan 1882 . . . . . . . . . 10 Ⅎ𝑏((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)))
41 nfv 1893 . . . . . . . . . 10 Ⅎ𝑏(𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)
4240, 41nfan 1882 . . . . . . . . 9 Ⅎ𝑏(((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋))
43 nfv 1893 . . . . . . . . 9 Ⅎ𝑏{𝑚, 𝑛} = {𝑥, 𝑦}
44 vex 3439 . . . . . . . . . . . 12 𝑚 ∈ V
45 vex 3439 . . . . . . . . . . . 12 𝑛 ∈ V
46 vex 3439 . . . . . . . . . . . 12 𝑎 ∈ V
47 vex 3439 . . . . . . . . . . . 12 𝑏 ∈ V
4844, 45, 46, 47preq12b 4690 . . . . . . . . . . 11 ({𝑚, 𝑛} = {𝑎, 𝑏} ↔ ((𝑚 = 𝑎 ∧ 𝑛 = 𝑏) ∨ (𝑚 = 𝑏 ∧ 𝑛 = 𝑎)))
49 opeq1 4712 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 𝑚 → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑗⟩)
5049eqeq1d 2796 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑚 → (⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑚, 𝑗⟩ = ⟨𝑎, 𝑏⟩))
5150anbi1d 629 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑚 → ((⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑚, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
52512exbidv 1903 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑚 → (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑎∃𝑏(⟨𝑚, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
5349eqeq1d 2796 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑚 → (⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑚, 𝑗⟩ = ⟨𝑥, 𝑦⟩))
5452, 53imbi12d 346 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑚 → ((∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) ↔ (∃𝑎∃𝑏(⟨𝑚, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑗⟩ = ⟨𝑥, 𝑦⟩)))
55 opeq2 4713 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑛 → ⟨𝑚, 𝑗⟩ = ⟨𝑚, 𝑛⟩)
5655eqeq1d 2796 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑛 → (⟨𝑚, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩))
5756anbi1d 629 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑛 → ((⟨𝑚, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
58572exbidv 1903 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑛 → (∃𝑎∃𝑏(⟨𝑚, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
5955eqeq1d 2796 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑛 → (⟨𝑚, 𝑗⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩))
6058, 59imbi12d 346 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑛 → ((∃𝑎∃𝑏(⟨𝑚, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑗⟩ = ⟨𝑥, 𝑦⟩) ↔ (∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩)))
6154, 60rspc2v 3570 . . . . . . . . . . . . . . . 16 ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → (∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) → (∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩)))
62 pm3.22 460 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)))
63623adant2 1124 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑎 ∧ 𝑛 = 𝑏) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)))
6463adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑎 ∧ 𝑛 = 𝑏) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝜑) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)))
65 eqidd 2795 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑎 ∧ 𝑛 = 𝑏) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩)
66 sbceq1a 3718 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = 𝑚 → (𝜑 ↔ [𝑚 / 𝑎]𝜑))
6766equcoms 2005 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑚 = 𝑎 → (𝜑 ↔ [𝑚 / 𝑎]𝜑))
68 sbceq1a 3718 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 = 𝑛 → ([𝑚 / 𝑎]𝜑 ↔ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑))
6968equcoms 2005 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = 𝑏 → ([𝑚 / 𝑎]𝜑 ↔ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑))
7067, 69sylan9bb 510 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑚 = 𝑎 ∧ 𝑛 = 𝑏) → (𝜑 ↔ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑))
71703ad2ant2 1127 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑎 ∧ 𝑛 = 𝑏) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝜑 ↔ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑))
7271biimpa 477 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑎 ∧ 𝑛 = 𝑏) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝜑) → [𝑛 / 𝑏][𝑚 / 𝑎]𝜑)
7364, 65, 72jca32 516 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑎 ∧ 𝑛 = 𝑏) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝜑) → (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)) ∧ (⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩ ∧ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑)))
74 nfv 1893 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ⅎ𝑎⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩
75 nfcv 2948 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Ⅎ𝑎𝑛
76 nfsbc1v 3727 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Ⅎ𝑎[𝑚 / 𝑎]𝜑
7775, 76nfsbc 3729 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ⅎ𝑎[𝑛 / 𝑏][𝑚 / 𝑎]𝜑
7874, 77nfan 1882 . . . . . . . . . . . . . . . . . . . . . . . 24 Ⅎ𝑎(⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩ ∧ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑)
79 nfv 1893 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ⅎ𝑏⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩
80 nfsbc1v 3727 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ⅎ𝑏[𝑛 / 𝑏][𝑚 / 𝑎]𝜑
8179, 80nfan 1882 . . . . . . . . . . . . . . . . . . . . . . . 24 Ⅎ𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩ ∧ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑)
82 opeq12 4714 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑎 = 𝑚 ∧ 𝑏 = 𝑛) → ⟨𝑎, 𝑏⟩ = ⟨𝑚, 𝑛⟩)
8382eqeq2d 2804 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 = 𝑚 ∧ 𝑏 = 𝑛) → (⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩))
8466, 68sylan9bb 510 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 = 𝑚 ∧ 𝑏 = 𝑛) → (𝜑 ↔ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑))
8583, 84anbi12d 630 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 = 𝑚 ∧ 𝑏 = 𝑛) → ((⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩ ∧ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑)))
8685adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑎 = 𝑚 ∧ 𝑏 = 𝑛)) → ((⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩ ∧ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑)))
8778, 81, 86spc2ed 3542 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)) → ((⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩ ∧ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑) → ∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
8887imp 407 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)) ∧ (⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩ ∧ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑)) → ∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑))
89 pm2.27 42 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ((∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩))
9073, 88, 893syl 18 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑎 ∧ 𝑛 = 𝑏) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝜑) → ((∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩))
91 oppr 42795 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑚 ∈ V ∧ 𝑛 ∈ V) → (⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩ → {𝑚, 𝑛} = {𝑥, 𝑦}))
9291el2v 3443 . . . . . . . . . . . . . . . . . . . . 21 (⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩ → {𝑚, 𝑛} = {𝑥, 𝑦})
9390, 92syl6 35 . . . . . . . . . . . . . . . . . . . 20 ((((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑎 ∧ 𝑛 = 𝑏) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝜑) → ((∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩) → {𝑚, 𝑛} = {𝑥, 𝑦}))
9493ex 413 . . . . . . . . . . . . . . . . . . 19 (((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑎 ∧ 𝑛 = 𝑏) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝜑 → ((∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩) → {𝑚, 𝑛} = {𝑥, 𝑦})))
9594com23 86 . . . . . . . . . . . . . . . . . 18 (((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑎 ∧ 𝑛 = 𝑏) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))
96953exp 1112 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → ((𝑚 = 𝑎 ∧ 𝑛 = 𝑏) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))))
9796com24 95 . . . . . . . . . . . . . . . 16 ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → ((∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑚 = 𝑎 ∧ 𝑛 = 𝑏) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))))
9861, 97syld 47 . . . . . . . . . . . . . . 15 ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → (∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑚 = 𝑎 ∧ 𝑛 = 𝑏) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))))
9998com13 88 . . . . . . . . . . . . . 14 ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) → ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → ((𝑚 = 𝑎 ∧ 𝑛 = 𝑏) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))))
10099a1d 25 . . . . . . . . . . . . 13 ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → (∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) → ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → ((𝑚 = 𝑎 ∧ 𝑛 = 𝑏) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦}))))))
101100imp42 427 . . . . . . . . . . . 12 ((((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)) → ((𝑚 = 𝑎 ∧ 𝑛 = 𝑏) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))
102 opeq1 4712 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = 𝑛 → ⟨𝑖, 𝑗⟩ = ⟨𝑛, 𝑗⟩)
103102eqeq1d 2796 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 𝑛 → (⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑛, 𝑗⟩ = ⟨𝑎, 𝑏⟩))
104103anbi1d 629 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑛 → ((⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑛, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
1051042exbidv 1903 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑛 → (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑎∃𝑏(⟨𝑛, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
106102eqeq1d 2796 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑛 → (⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑛, 𝑗⟩ = ⟨𝑥, 𝑦⟩))
107105, 106imbi12d 346 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑛 → ((∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) ↔ (∃𝑎∃𝑏(⟨𝑛, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑗⟩ = ⟨𝑥, 𝑦⟩)))
108 opeq2 4713 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑚 → ⟨𝑛, 𝑗⟩ = ⟨𝑛, 𝑚⟩)
109108eqeq1d 2796 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑚 → (⟨𝑛, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩))
110109anbi1d 629 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑚 → ((⟨𝑛, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
1111102exbidv 1903 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑚 → (∃𝑎∃𝑏(⟨𝑛, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
112108eqeq1d 2796 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑚 → (⟨𝑛, 𝑗⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩))
113111, 112imbi12d 346 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑚 → ((∃𝑎∃𝑏(⟨𝑛, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑗⟩ = ⟨𝑥, 𝑦⟩) ↔ (∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩)))
114107, 113rspc2v 3570 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ 𝑋 ∧ 𝑚 ∈ 𝑋) → (∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) → (∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩)))
115114ancoms 459 . . . . . . . . . . . . . . . 16 ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → (∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) → (∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩)))
116 pm3.22 460 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → (𝑛 ∈ 𝑋 ∧ 𝑚 ∈ 𝑋))
117116anim1ci 615 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑛 ∈ 𝑋 ∧ 𝑚 ∈ 𝑋)))
1181173adant2 1124 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑏 ∧ 𝑛 = 𝑎) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑛 ∈ 𝑋 ∧ 𝑚 ∈ 𝑋)))
119118adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑏 ∧ 𝑛 = 𝑎) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝜑) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑛 ∈ 𝑋 ∧ 𝑚 ∈ 𝑋)))
120 eqidd 2795 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑏 ∧ 𝑛 = 𝑎) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩)
121 sbceq1a 3718 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 = 𝑚 → (𝜑 ↔ [𝑚 / 𝑏]𝜑))
122121equcoms 2005 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑚 = 𝑏 → (𝜑 ↔ [𝑚 / 𝑏]𝜑))
123 sbceq1a 3718 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = 𝑛 → ([𝑚 / 𝑏]𝜑 ↔ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑))
124123equcoms 2005 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = 𝑎 → ([𝑚 / 𝑏]𝜑 ↔ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑))
125122, 124sylan9bb 510 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑚 = 𝑏 ∧ 𝑛 = 𝑎) → (𝜑 ↔ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑))
1261253ad2ant2 1127 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑏 ∧ 𝑛 = 𝑎) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝜑 ↔ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑))
127126biimpa 477 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑏 ∧ 𝑛 = 𝑎) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝜑) → [𝑛 / 𝑎][𝑚 / 𝑏]𝜑)
128119, 120, 127jca32 516 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑏 ∧ 𝑛 = 𝑎) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝜑) → (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑛 ∈ 𝑋 ∧ 𝑚 ∈ 𝑋)) ∧ (⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩ ∧ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑)))
129 nfv 1893 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ⅎ𝑎⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩
130 nfsbc1v 3727 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ⅎ𝑎[𝑛 / 𝑎][𝑚 / 𝑏]𝜑
131129, 130nfan 1882 . . . . . . . . . . . . . . . . . . . . . . . 24 Ⅎ𝑎(⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩ ∧ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑)
132 nfv 1893 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ⅎ𝑏⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩
133 nfcv 2948 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Ⅎ𝑏𝑛
134 nfsbc1v 3727 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Ⅎ𝑏[𝑚 / 𝑏]𝜑
135133, 134nfsbc 3729 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ⅎ𝑏[𝑛 / 𝑎][𝑚 / 𝑏]𝜑
136132, 135nfan 1882 . . . . . . . . . . . . . . . . . . . . . . . 24 Ⅎ𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩ ∧ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑)
137 opeq12 4714 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑎 = 𝑛 ∧ 𝑏 = 𝑚) → ⟨𝑎, 𝑏⟩ = ⟨𝑛, 𝑚⟩)
138137eqeq2d 2804 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 = 𝑛 ∧ 𝑏 = 𝑚) → (⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩))
139121, 123sylan9bbr 511 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 = 𝑛 ∧ 𝑏 = 𝑚) → (𝜑 ↔ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑))
140138, 139anbi12d 630 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 = 𝑛 ∧ 𝑏 = 𝑚) → ((⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩ ∧ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑)))
141140adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑎 = 𝑛 ∧ 𝑏 = 𝑚)) → ((⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩ ∧ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑)))
142131, 136, 141spc2ed 3542 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑛 ∈ 𝑋 ∧ 𝑚 ∈ 𝑋)) → ((⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩ ∧ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑) → ∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
143142imp 407 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑛 ∈ 𝑋 ∧ 𝑚 ∈ 𝑋)) ∧ (⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩ ∧ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑)) → ∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑))
144 pm2.27 42 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ((∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩))
145128, 143, 1443syl 18 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑏 ∧ 𝑛 = 𝑎) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝜑) → ((∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩))
146 prcom 4577 . . . . . . . . . . . . . . . . . . . . . 22 {𝑛, 𝑚} = {𝑚, 𝑛}
147 oppr 42795 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ V ∧ 𝑚 ∈ V) → (⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩ → {𝑛, 𝑚} = {𝑥, 𝑦}))
148147el2v 3443 . . . . . . . . . . . . . . . . . . . . . 22 (⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩ → {𝑛, 𝑚} = {𝑥, 𝑦})
149146, 148syl5eqr 2844 . . . . . . . . . . . . . . . . . . . . 21 (⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩ → {𝑚, 𝑛} = {𝑥, 𝑦})
150145, 149syl6 35 . . . . . . . . . . . . . . . . . . . 20 ((((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑏 ∧ 𝑛 = 𝑎) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝜑) → ((∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩) → {𝑚, 𝑛} = {𝑥, 𝑦}))
151150ex 413 . . . . . . . . . . . . . . . . . . 19 (((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑏 ∧ 𝑛 = 𝑎) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝜑 → ((∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩) → {𝑚, 𝑛} = {𝑥, 𝑦})))
152151com23 86 . . . . . . . . . . . . . . . . . 18 (((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑏 ∧ 𝑛 = 𝑎) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))
1531523exp 1112 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → ((𝑚 = 𝑏 ∧ 𝑛 = 𝑎) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))))
154153com24 95 . . . . . . . . . . . . . . . 16 ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → ((∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑚 = 𝑏 ∧ 𝑛 = 𝑎) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))))
155115, 154syld 47 . . . . . . . . . . . . . . 15 ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → (∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑚 = 𝑏 ∧ 𝑛 = 𝑎) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))))
156155com13 88 . . . . . . . . . . . . . 14 ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) → ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → ((𝑚 = 𝑏 ∧ 𝑛 = 𝑎) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))))
157156a1d 25 . . . . . . . . . . . . 13 ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → (∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) → ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → ((𝑚 = 𝑏 ∧ 𝑛 = 𝑎) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦}))))))
158157imp42 427 . . . . . . . . . . . 12 ((((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)) → ((𝑚 = 𝑏 ∧ 𝑛 = 𝑎) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))
159101, 158jaod 854 . . . . . . . . . . 11 ((((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)) → (((𝑚 = 𝑎 ∧ 𝑛 = 𝑏) ∨ (𝑚 = 𝑏 ∧ 𝑛 = 𝑎)) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))
16048, 159syl5bi 243 . . . . . . . . . 10 ((((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)) → ({𝑚, 𝑛} = {𝑎, 𝑏} → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))
161160impd 411 . . . . . . . . 9 ((((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)) → (({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑦}))
16242, 43, 161exlimd 2182 . . . . . . . 8 ((((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)) → (∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑦}))
16327, 28, 162exlimd 2182 . . . . . . 7 ((((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)) → (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑦}))
164163ralrimivva 3157 . . . . . 6 (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) → ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑦}))
165 preq1 4578 . . . . . . . . . . 11 (𝑣 = 𝑥 → {𝑣, 𝑤} = {𝑥, 𝑤})
166165eqeq1d 2796 . . . . . . . . . 10 (𝑣 = 𝑥 → ({𝑣, 𝑤} = {𝑎, 𝑏} ↔ {𝑥, 𝑤} = {𝑎, 𝑏}))
167166anbi1d 629 . . . . . . . . 9 (𝑣 = 𝑥 → (({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ↔ ({𝑥, 𝑤} = {𝑎, 𝑏} ∧ 𝜑)))
1681672exbidv 1903 . . . . . . . 8 (𝑣 = 𝑥 → (∃𝑎∃𝑏({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ↔ ∃𝑎∃𝑏({𝑥, 𝑤} = {𝑎, 𝑏} ∧ 𝜑)))
169165eqeq2d 2804 . . . . . . . . . 10 (𝑣 = 𝑥 → ({𝑚, 𝑛} = {𝑣, 𝑤} ↔ {𝑚, 𝑛} = {𝑥, 𝑤}))
170169imbi2d 342 . . . . . . . . 9 (𝑣 = 𝑥 → ((∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑣, 𝑤}) ↔ (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑤})))
1711702ralbidv 3165 . . . . . . . 8 (𝑣 = 𝑥 → (∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑣, 𝑤}) ↔ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑤})))
172168, 171anbi12d 630 . . . . . . 7 (𝑣 = 𝑥 → ((∃𝑎∃𝑏({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑣, 𝑤})) ↔ (∃𝑎∃𝑏({𝑥, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑤}))))
173 preq2 4579 . . . . . . . . . . 11 (𝑤 = 𝑦 → {𝑥, 𝑤} = {𝑥, 𝑦})
174173eqeq1d 2796 . . . . . . . . . 10 (𝑤 = 𝑦 → ({𝑥, 𝑤} = {𝑎, 𝑏} ↔ {𝑥, 𝑦} = {𝑎, 𝑏}))
175174anbi1d 629 . . . . . . . . 9 (𝑤 = 𝑦 → (({𝑥, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ↔ ({𝑥, 𝑦} = {𝑎, 𝑏} ∧ 𝜑)))
1761752exbidv 1903 . . . . . . . 8 (𝑤 = 𝑦 → (∃𝑎∃𝑏({𝑥, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ↔ ∃𝑎∃𝑏({𝑥, 𝑦} = {𝑎, 𝑏} ∧ 𝜑)))
177173eqeq2d 2804 . . . . . . . . . 10 (𝑤 = 𝑦 → ({𝑚, 𝑛} = {𝑥, 𝑤} ↔ {𝑚, 𝑛} = {𝑥, 𝑦}))
178177imbi2d 342 . . . . . . . . 9 (𝑤 = 𝑦 → ((∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑤}) ↔ (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑦})))
1791782ralbidv 3165 . . . . . . . 8 (𝑤 = 𝑦 → (∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑤}) ↔ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑦})))
180176, 179anbi12d 630 . . . . . . 7 (𝑤 = 𝑦 → ((∃𝑎∃𝑏({𝑥, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑤})) ↔ (∃𝑎∃𝑏({𝑥, 𝑦} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑦}))))
181172, 180rspc2ev 3572 . . . . . 6 ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (∃𝑎∃𝑏({𝑥, 𝑦} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑦}))) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑋 (∃𝑎∃𝑏({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑣, 𝑤})))
1828, 9, 15, 164, 181syl112anc 1367 . . . . 5 (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑋 (∃𝑎∃𝑏({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑣, 𝑤})))
183182ex 413 . . . 4 ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑋 (∃𝑎∃𝑏({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑣, 𝑤}))))
184183rexlimivv 3254 . . 3 (∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑋 (∃𝑎∃𝑏({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑣, 𝑤})))
185 eqeq1 2798 . . . . . 6 (𝑝 = {𝑣, 𝑤} → (𝑝 = {𝑎, 𝑏} ↔ {𝑣, 𝑤} = {𝑎, 𝑏}))
186185anbi1d 629 . . . . 5 (𝑝 = {𝑣, 𝑤} → ((𝑝 = {𝑎, 𝑏} ∧ 𝜑) ↔ ({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑)))
1871862exbidv 1903 . . . 4 (𝑝 = {𝑣, 𝑤} → (∃𝑎∃𝑏(𝑝 = {𝑎, 𝑏} ∧ 𝜑) ↔ ∃𝑎∃𝑏({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑)))
188 eqeq1 2798 . . . . . 6 (𝑝 = {𝑚, 𝑛} → (𝑝 = {𝑎, 𝑏} ↔ {𝑚, 𝑛} = {𝑎, 𝑏}))
189188anbi1d 629 . . . . 5 (𝑝 = {𝑚, 𝑛} → ((𝑝 = {𝑎, 𝑏} ∧ 𝜑) ↔ ({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑)))
1901892exbidv 1903 . . . 4 (𝑝 = {𝑚, 𝑛} → (∃𝑎∃𝑏(𝑝 = {𝑎, 𝑏} ∧ 𝜑) ↔ ∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑)))
191187, 190reupr 43180 . . 3 (𝑋 ∈ 𝑉 → (∃!𝑝 ∈ (Pairs‘𝑋)∃𝑎∃𝑏(𝑝 = {𝑎, 𝑏} ∧ 𝜑) ↔ ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑋 (∃𝑎∃𝑏({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑣, 𝑤}))))
192184, 191syl5ibr 247 . 2 (𝑋 ∈ 𝑉 → (∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)) → ∃!𝑝 ∈ (Pairs‘𝑋)∃𝑎∃𝑏(𝑝 = {𝑎, 𝑏} ∧ 𝜑)))
1937, 192syl5bi 243 1 (𝑋 ∈ 𝑉 → (∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎∃𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ∃!𝑝 ∈ (Pairs‘𝑋)∃𝑎∃𝑏(𝑝 = {𝑎, 𝑏} ∧ 𝜑)))
Colors of variables: wff setvar class
Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∨ wo 842   ∧ w3a 1080   = wceq 1522  ∃wex 1762   ∈ wcel 2080  ∀wral 3104  ∃wrex 3105  ∃!wreu 3106  Vcvv 3436  [wsbc 3707  {cpr 4476  ⟨cop 4480   × cxp 5444  ‘cfv 6228  Pairscspr 43135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-8 2082  ax-9 2090  ax-10 2111  ax-11 2125  ax-12 2140  ax-13 2343  ax-ext 2768  ax-rep 5084  ax-sep 5097  ax-nul 5104  ax-pow 5160  ax-pr 5224  ax-un 7322
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-fal 1535  df-ex 1763  df-nf 1767  df-sb 2042  df-mo 2575  df-eu 2611  df-clab 2775  df-cleq 2787  df-clel 2862  df-nfc 2934  df-ne 2984  df-ral 3109  df-rex 3110  df-reu 3111  df-rab 3113  df-v 3438  df-sbc 3708  df-csb 3814  df-dif 3864  df-un 3866  df-in 3868  df-ss 3876  df-nul 4214  df-if 4384  df-pw 4457  df-sn 4475  df-pr 4477  df-op 4481  df-uni 4748  df-iun 4829  df-br 4965  df-opab 5027  df-mpt 5044  df-id 5351  df-xp 5452  df-rel 5453  df-cnv 5454  df-co 5455  df-dm 5456  df-rn 5457  df-res 5458  df-ima 5459  df-iota 6192  df-fun 6230  df-fn 6231  df-f 6232  df-f1 6233  df-fo 6234  df-f1o 6235  df-fv 6236  df-spr 43136
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator