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 43737
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 2825 . . . . 5 (𝑝 = ⟨𝑥, 𝑦⟩ → (𝑝 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))
21anbi1d 631 . . . 4 (𝑝 = ⟨𝑥, 𝑦⟩ → ((𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
322exbidv 1925 . . 3 (𝑝 = ⟨𝑥, 𝑦⟩ → (∃𝑎∃𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
4 eqeq1 2825 . . . . 5 (𝑝 = ⟨𝑖, 𝑗⟩ → (𝑝 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩))
54anbi1d 631 . . . 4 (𝑝 = ⟨𝑖, 𝑗⟩ → ((𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
652exbidv 1925 . . 3 (𝑝 = ⟨𝑖, 𝑗⟩ → (∃𝑎∃𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
73, 6reuop 6144 . 2 (∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎∃𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)))
8 simpll 765 . . . . . 6 (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) → 𝑥 ∈ 𝑋)
9 simplr 767 . . . . . 6 (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) → 𝑦 ∈ 𝑋)
10 oppr 43314 . . . . . . . . . . 11 ((𝑥 ∈ V ∧ 𝑦 ∈ V) → (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ → {𝑥, 𝑦} = {𝑎, 𝑏}))
1110el2v 3501 . . . . . . . . . 10 (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ → {𝑥, 𝑦} = {𝑎, 𝑏})
1211anim1i 616 . . . . . . . . 9 ((⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ({𝑥, 𝑦} = {𝑎, 𝑏} ∧ 𝜑))
13122eximi 1836 . . . . . . . 8 (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ∃𝑎∃𝑏({𝑥, 𝑦} = {𝑎, 𝑏} ∧ 𝜑))
1413adantr 483 . . . . . . 7 ((∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)) → ∃𝑎∃𝑏({𝑥, 𝑦} = {𝑎, 𝑏} ∧ 𝜑))
1514adantl 484 . . . . . 6 (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) → ∃𝑎∃𝑏({𝑥, 𝑦} = {𝑎, 𝑏} ∧ 𝜑))
16 nfv 1915 . . . . . . . . . 10 Ⅎ𝑎(𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)
17 nfe1 2154 . . . . . . . . . . 11 Ⅎ𝑎∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)
18 nfcv 2977 . . . . . . . . . . . 12 Ⅎ𝑎𝑋
19 nfe1 2154 . . . . . . . . . . . . . 14 Ⅎ𝑎∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)
20 nfv 1915 . . . . . . . . . . . . . 14 Ⅎ𝑎⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩
2119, 20nfim 1897 . . . . . . . . . . . . 13 Ⅎ𝑎(∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)
2218, 21nfralw 3225 . . . . . . . . . . . 12 Ⅎ𝑎∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)
2318, 22nfralw 3225 . . . . . . . . . . 11 Ⅎ𝑎∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)
2417, 23nfan 1900 . . . . . . . . . 10 Ⅎ𝑎(∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))
2516, 24nfan 1900 . . . . . . . . 9 Ⅎ𝑎((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)))
26 nfv 1915 . . . . . . . . 9 Ⅎ𝑎(𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)
2725, 26nfan 1900 . . . . . . . 8 Ⅎ𝑎(((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋))
28 nfv 1915 . . . . . . . 8 Ⅎ𝑎{𝑚, 𝑛} = {𝑥, 𝑦}
29 nfv 1915 . . . . . . . . . . 11 Ⅎ𝑏(𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)
30 nfe1 2154 . . . . . . . . . . . . 13 Ⅎ𝑏∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)
3130nfex 2343 . . . . . . . . . . . 12 Ⅎ𝑏∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)
32 nfcv 2977 . . . . . . . . . . . . 13 Ⅎ𝑏𝑋
33 nfe1 2154 . . . . . . . . . . . . . . . 16 Ⅎ𝑏∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)
3433nfex 2343 . . . . . . . . . . . . . . 15 Ⅎ𝑏∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)
35 nfv 1915 . . . . . . . . . . . . . . 15 Ⅎ𝑏⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩
3634, 35nfim 1897 . . . . . . . . . . . . . 14 Ⅎ𝑏(∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)
3732, 36nfralw 3225 . . . . . . . . . . . . 13 Ⅎ𝑏∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)
3832, 37nfralw 3225 . . . . . . . . . . . 12 Ⅎ𝑏∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)
3931, 38nfan 1900 . . . . . . . . . . 11 Ⅎ𝑏(∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))
4029, 39nfan 1900 . . . . . . . . . 10 Ⅎ𝑏((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)))
41 nfv 1915 . . . . . . . . . 10 Ⅎ𝑏(𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)
4240, 41nfan 1900 . . . . . . . . 9 Ⅎ𝑏(((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋))
43 nfv 1915 . . . . . . . . 9 Ⅎ𝑏{𝑚, 𝑛} = {𝑥, 𝑦}
44 vex 3497 . . . . . . . . . . . 12 𝑚 ∈ V
45 vex 3497 . . . . . . . . . . . 12 𝑛 ∈ V
46 vex 3497 . . . . . . . . . . . 12 𝑎 ∈ V
47 vex 3497 . . . . . . . . . . . 12 𝑏 ∈ V
4844, 45, 46, 47preq12b 4781 . . . . . . . . . . 11 ({𝑚, 𝑛} = {𝑎, 𝑏} ↔ ((𝑚 = 𝑎 ∧ 𝑛 = 𝑏) ∨ (𝑚 = 𝑏 ∧ 𝑛 = 𝑎)))
49 opeq1 4803 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 𝑚 → ⟨𝑖, 𝑗⟩ = ⟨𝑚, 𝑗⟩)
5049eqeq1d 2823 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑚 → (⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑚, 𝑗⟩ = ⟨𝑎, 𝑏⟩))
5150anbi1d 631 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑚 → ((⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑚, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
52512exbidv 1925 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑚 → (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑎∃𝑏(⟨𝑚, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
5349eqeq1d 2823 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑚 → (⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑚, 𝑗⟩ = ⟨𝑥, 𝑦⟩))
5452, 53imbi12d 347 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑚 → ((∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) ↔ (∃𝑎∃𝑏(⟨𝑚, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑗⟩ = ⟨𝑥, 𝑦⟩)))
55 opeq2 4804 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑛 → ⟨𝑚, 𝑗⟩ = ⟨𝑚, 𝑛⟩)
5655eqeq1d 2823 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑛 → (⟨𝑚, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩))
5756anbi1d 631 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑛 → ((⟨𝑚, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
58572exbidv 1925 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑛 → (∃𝑎∃𝑏(⟨𝑚, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
5955eqeq1d 2823 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑛 → (⟨𝑚, 𝑗⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩))
6058, 59imbi12d 347 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑛 → ((∃𝑎∃𝑏(⟨𝑚, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑗⟩ = ⟨𝑥, 𝑦⟩) ↔ (∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩)))
6154, 60rspc2v 3633 . . . . . . . . . . . . . . . 16 ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → (∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) → (∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩)))
62 pm3.22 462 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)))
63623adant2 1127 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑎 ∧ 𝑛 = 𝑏) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)))
6463adantr 483 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑎 ∧ 𝑛 = 𝑏) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝜑) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)))
65 eqidd 2822 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑎 ∧ 𝑛 = 𝑏) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩)
66 sbceq1a 3783 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = 𝑚 → (𝜑 ↔ [𝑚 / 𝑎]𝜑))
6766equcoms 2027 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑚 = 𝑎 → (𝜑 ↔ [𝑚 / 𝑎]𝜑))
68 sbceq1a 3783 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 = 𝑛 → ([𝑚 / 𝑎]𝜑 ↔ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑))
6968equcoms 2027 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = 𝑏 → ([𝑚 / 𝑎]𝜑 ↔ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑))
7067, 69sylan9bb 512 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑚 = 𝑎 ∧ 𝑛 = 𝑏) → (𝜑 ↔ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑))
71703ad2ant2 1130 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑎 ∧ 𝑛 = 𝑏) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝜑 ↔ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑))
7271biimpa 479 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑎 ∧ 𝑛 = 𝑏) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝜑) → [𝑛 / 𝑏][𝑚 / 𝑎]𝜑)
7364, 65, 72jca32 518 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑎 ∧ 𝑛 = 𝑏) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝜑) → (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)) ∧ (⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩ ∧ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑)))
74 nfv 1915 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ⅎ𝑎⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩
75 nfcv 2977 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Ⅎ𝑎𝑛
76 nfsbc1v 3792 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Ⅎ𝑎[𝑚 / 𝑎]𝜑
7775, 76nfsbcw 3794 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ⅎ𝑎[𝑛 / 𝑏][𝑚 / 𝑎]𝜑
7874, 77nfan 1900 . . . . . . . . . . . . . . . . . . . . . . . 24 Ⅎ𝑎(⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩ ∧ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑)
79 nfv 1915 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ⅎ𝑏⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩
80 nfsbc1v 3792 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ⅎ𝑏[𝑛 / 𝑏][𝑚 / 𝑎]𝜑
8179, 80nfan 1900 . . . . . . . . . . . . . . . . . . . . . . . 24 Ⅎ𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩ ∧ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑)
82 opeq12 4805 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑎 = 𝑚 ∧ 𝑏 = 𝑛) → ⟨𝑎, 𝑏⟩ = ⟨𝑚, 𝑛⟩)
8382eqeq2d 2832 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 = 𝑚 ∧ 𝑏 = 𝑛) → (⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩))
8466, 68sylan9bb 512 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 = 𝑚 ∧ 𝑏 = 𝑛) → (𝜑 ↔ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑))
8583, 84anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 = 𝑚 ∧ 𝑏 = 𝑛) → ((⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩ ∧ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑)))
8685adantl 484 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑎 = 𝑚 ∧ 𝑏 = 𝑛)) → ((⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩ ∧ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑)))
8778, 81, 86spc2ed 3602 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)) → ((⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩ ∧ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑) → ∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
8887imp 409 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)) ∧ (⟨𝑚, 𝑛⟩ = ⟨𝑚, 𝑛⟩ ∧ [𝑛 / 𝑏][𝑚 / 𝑎]𝜑)) → ∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑))
89 pm2.27 42 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ((∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩))
9073, 88, 893syl 18 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑎 ∧ 𝑛 = 𝑏) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝜑) → ((∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩))
91 oppr 43314 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑚 ∈ V ∧ 𝑛 ∈ V) → (⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩ → {𝑚, 𝑛} = {𝑥, 𝑦}))
9291el2v 3501 . . . . . . . . . . . . . . . . . . . . 21 (⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩ → {𝑚, 𝑛} = {𝑥, 𝑦})
9390, 92syl6 35 . . . . . . . . . . . . . . . . . . . 20 ((((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑎 ∧ 𝑛 = 𝑏) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝜑) → ((∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩) → {𝑚, 𝑛} = {𝑥, 𝑦}))
9493ex 415 . . . . . . . . . . . . . . . . . . 19 (((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑎 ∧ 𝑛 = 𝑏) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝜑 → ((∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩) → {𝑚, 𝑛} = {𝑥, 𝑦})))
9594com23 86 . . . . . . . . . . . . . . . . . 18 (((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑎 ∧ 𝑛 = 𝑏) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))
96953exp 1115 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → ((𝑚 = 𝑎 ∧ 𝑛 = 𝑏) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))))
9796com24 95 . . . . . . . . . . . . . . . 16 ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → ((∃𝑎∃𝑏(⟨𝑚, 𝑛⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑚, 𝑛⟩ = ⟨𝑥, 𝑦⟩) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑚 = 𝑎 ∧ 𝑛 = 𝑏) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))))
9861, 97syld 47 . . . . . . . . . . . . . . 15 ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → (∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑚 = 𝑎 ∧ 𝑛 = 𝑏) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))))
9998com13 88 . . . . . . . . . . . . . 14 ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) → ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → ((𝑚 = 𝑎 ∧ 𝑛 = 𝑏) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))))
10099a1d 25 . . . . . . . . . . . . 13 ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → (∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) → ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → ((𝑚 = 𝑎 ∧ 𝑛 = 𝑏) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦}))))))
101100imp42 429 . . . . . . . . . . . 12 ((((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)) → ((𝑚 = 𝑎 ∧ 𝑛 = 𝑏) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))
102 opeq1 4803 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = 𝑛 → ⟨𝑖, 𝑗⟩ = ⟨𝑛, 𝑗⟩)
103102eqeq1d 2823 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 𝑛 → (⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑛, 𝑗⟩ = ⟨𝑎, 𝑏⟩))
104103anbi1d 631 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑛 → ((⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑛, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
1051042exbidv 1925 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑛 → (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑎∃𝑏(⟨𝑛, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
106102eqeq1d 2823 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑛 → (⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑛, 𝑗⟩ = ⟨𝑥, 𝑦⟩))
107105, 106imbi12d 347 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑛 → ((∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) ↔ (∃𝑎∃𝑏(⟨𝑛, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑗⟩ = ⟨𝑥, 𝑦⟩)))
108 opeq2 4804 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑚 → ⟨𝑛, 𝑗⟩ = ⟨𝑛, 𝑚⟩)
109108eqeq1d 2823 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑚 → (⟨𝑛, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩))
110109anbi1d 631 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑚 → ((⟨𝑛, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
1111102exbidv 1925 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑚 → (∃𝑎∃𝑏(⟨𝑛, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
112108eqeq1d 2823 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑚 → (⟨𝑛, 𝑗⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩))
113111, 112imbi12d 347 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑚 → ((∃𝑎∃𝑏(⟨𝑛, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑗⟩ = ⟨𝑥, 𝑦⟩) ↔ (∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩)))
114107, 113rspc2v 3633 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ 𝑋 ∧ 𝑚 ∈ 𝑋) → (∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) → (∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩)))
115114ancoms 461 . . . . . . . . . . . . . . . 16 ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → (∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) → (∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩)))
116 pm3.22 462 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → (𝑛 ∈ 𝑋 ∧ 𝑚 ∈ 𝑋))
117116anim1ci 617 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑛 ∈ 𝑋 ∧ 𝑚 ∈ 𝑋)))
1181173adant2 1127 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑏 ∧ 𝑛 = 𝑎) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑛 ∈ 𝑋 ∧ 𝑚 ∈ 𝑋)))
119118adantr 483 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑏 ∧ 𝑛 = 𝑎) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝜑) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑛 ∈ 𝑋 ∧ 𝑚 ∈ 𝑋)))
120 eqidd 2822 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑏 ∧ 𝑛 = 𝑎) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩)
121 sbceq1a 3783 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 = 𝑚 → (𝜑 ↔ [𝑚 / 𝑏]𝜑))
122121equcoms 2027 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑚 = 𝑏 → (𝜑 ↔ [𝑚 / 𝑏]𝜑))
123 sbceq1a 3783 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = 𝑛 → ([𝑚 / 𝑏]𝜑 ↔ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑))
124123equcoms 2027 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = 𝑎 → ([𝑚 / 𝑏]𝜑 ↔ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑))
125122, 124sylan9bb 512 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑚 = 𝑏 ∧ 𝑛 = 𝑎) → (𝜑 ↔ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑))
1261253ad2ant2 1130 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑏 ∧ 𝑛 = 𝑎) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝜑 ↔ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑))
127126biimpa 479 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑏 ∧ 𝑛 = 𝑎) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝜑) → [𝑛 / 𝑎][𝑚 / 𝑏]𝜑)
128119, 120, 127jca32 518 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑏 ∧ 𝑛 = 𝑎) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝜑) → (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑛 ∈ 𝑋 ∧ 𝑚 ∈ 𝑋)) ∧ (⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩ ∧ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑)))
129 nfv 1915 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ⅎ𝑎⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩
130 nfsbc1v 3792 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ⅎ𝑎[𝑛 / 𝑎][𝑚 / 𝑏]𝜑
131129, 130nfan 1900 . . . . . . . . . . . . . . . . . . . . . . . 24 Ⅎ𝑎(⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩ ∧ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑)
132 nfv 1915 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ⅎ𝑏⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩
133 nfcv 2977 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Ⅎ𝑏𝑛
134 nfsbc1v 3792 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Ⅎ𝑏[𝑚 / 𝑏]𝜑
135133, 134nfsbcw 3794 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ⅎ𝑏[𝑛 / 𝑎][𝑚 / 𝑏]𝜑
136132, 135nfan 1900 . . . . . . . . . . . . . . . . . . . . . . . 24 Ⅎ𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩ ∧ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑)
137 opeq12 4805 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑎 = 𝑛 ∧ 𝑏 = 𝑚) → ⟨𝑎, 𝑏⟩ = ⟨𝑛, 𝑚⟩)
138137eqeq2d 2832 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 = 𝑛 ∧ 𝑏 = 𝑚) → (⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩))
139121, 123sylan9bbr 513 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎 = 𝑛 ∧ 𝑏 = 𝑚) → (𝜑 ↔ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑))
140138, 139anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 = 𝑛 ∧ 𝑏 = 𝑚) → ((⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩ ∧ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑)))
141140adantl 484 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑎 = 𝑛 ∧ 𝑏 = 𝑚)) → ((⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩ ∧ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑)))
142131, 136, 141spc2ed 3602 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑛 ∈ 𝑋 ∧ 𝑚 ∈ 𝑋)) → ((⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩ ∧ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑) → ∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
143142imp 409 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑛 ∈ 𝑋 ∧ 𝑚 ∈ 𝑋)) ∧ (⟨𝑛, 𝑚⟩ = ⟨𝑛, 𝑚⟩ ∧ [𝑛 / 𝑎][𝑚 / 𝑏]𝜑)) → ∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑))
144 pm2.27 42 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ((∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩))
145128, 143, 1443syl 18 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑏 ∧ 𝑛 = 𝑎) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝜑) → ((∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩))
146 prcom 4668 . . . . . . . . . . . . . . . . . . . . . 22 {𝑛, 𝑚} = {𝑚, 𝑛}
147 oppr 43314 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑛 ∈ V ∧ 𝑚 ∈ V) → (⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩ → {𝑛, 𝑚} = {𝑥, 𝑦}))
148147el2v 3501 . . . . . . . . . . . . . . . . . . . . . 22 (⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩ → {𝑛, 𝑚} = {𝑥, 𝑦})
149146, 148syl5eqr 2870 . . . . . . . . . . . . . . . . . . . . 21 (⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩ → {𝑚, 𝑛} = {𝑥, 𝑦})
150145, 149syl6 35 . . . . . . . . . . . . . . . . . . . 20 ((((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑏 ∧ 𝑛 = 𝑎) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ 𝜑) → ((∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩) → {𝑚, 𝑛} = {𝑥, 𝑦}))
151150ex 415 . . . . . . . . . . . . . . . . . . 19 (((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑏 ∧ 𝑛 = 𝑎) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝜑 → ((∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩) → {𝑚, 𝑛} = {𝑥, 𝑦})))
152151com23 86 . . . . . . . . . . . . . . . . . 18 (((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) ∧ (𝑚 = 𝑏 ∧ 𝑛 = 𝑎) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))
1531523exp 1115 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → ((𝑚 = 𝑏 ∧ 𝑛 = 𝑎) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))))
154153com24 95 . . . . . . . . . . . . . . . 16 ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → ((∃𝑎∃𝑏(⟨𝑛, 𝑚⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑛, 𝑚⟩ = ⟨𝑥, 𝑦⟩) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑚 = 𝑏 ∧ 𝑛 = 𝑎) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))))
155115, 154syld 47 . . . . . . . . . . . . . . 15 ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → (∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((𝑚 = 𝑏 ∧ 𝑛 = 𝑎) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))))
156155com13 88 . . . . . . . . . . . . . 14 ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) → ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → ((𝑚 = 𝑏 ∧ 𝑛 = 𝑎) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))))
157156a1d 25 . . . . . . . . . . . . 13 ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → (∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩) → ((𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋) → ((𝑚 = 𝑏 ∧ 𝑛 = 𝑎) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦}))))))
158157imp42 429 . . . . . . . . . . . 12 ((((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)) → ((𝑚 = 𝑏 ∧ 𝑛 = 𝑎) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))
159101, 158jaod 855 . . . . . . . . . . 11 ((((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)) → (((𝑚 = 𝑎 ∧ 𝑛 = 𝑏) ∨ (𝑚 = 𝑏 ∧ 𝑛 = 𝑎)) → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))
16048, 159syl5bi 244 . . . . . . . . . 10 ((((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)) → ({𝑚, 𝑛} = {𝑎, 𝑏} → (𝜑 → {𝑚, 𝑛} = {𝑥, 𝑦})))
161160impd 413 . . . . . . . . 9 ((((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)) → (({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑦}))
16242, 43, 161exlimd 2218 . . . . . . . 8 ((((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)) → (∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑦}))
16327, 28, 162exlimd 2218 . . . . . . 7 ((((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) ∧ (𝑚 ∈ 𝑋 ∧ 𝑛 ∈ 𝑋)) → (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑦}))
164163ralrimivva 3191 . . . . . 6 (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) → ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑦}))
165 preq1 4669 . . . . . . . . . . 11 (𝑣 = 𝑥 → {𝑣, 𝑤} = {𝑥, 𝑤})
166165eqeq1d 2823 . . . . . . . . . 10 (𝑣 = 𝑥 → ({𝑣, 𝑤} = {𝑎, 𝑏} ↔ {𝑥, 𝑤} = {𝑎, 𝑏}))
167166anbi1d 631 . . . . . . . . 9 (𝑣 = 𝑥 → (({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ↔ ({𝑥, 𝑤} = {𝑎, 𝑏} ∧ 𝜑)))
1681672exbidv 1925 . . . . . . . 8 (𝑣 = 𝑥 → (∃𝑎∃𝑏({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ↔ ∃𝑎∃𝑏({𝑥, 𝑤} = {𝑎, 𝑏} ∧ 𝜑)))
169165eqeq2d 2832 . . . . . . . . . 10 (𝑣 = 𝑥 → ({𝑚, 𝑛} = {𝑣, 𝑤} ↔ {𝑚, 𝑛} = {𝑥, 𝑤}))
170169imbi2d 343 . . . . . . . . 9 (𝑣 = 𝑥 → ((∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑣, 𝑤}) ↔ (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑤})))
1711702ralbidv 3199 . . . . . . . 8 (𝑣 = 𝑥 → (∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑣, 𝑤}) ↔ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑤})))
172168, 171anbi12d 632 . . . . . . 7 (𝑣 = 𝑥 → ((∃𝑎∃𝑏({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑣, 𝑤})) ↔ (∃𝑎∃𝑏({𝑥, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑤}))))
173 preq2 4670 . . . . . . . . . . 11 (𝑤 = 𝑦 → {𝑥, 𝑤} = {𝑥, 𝑦})
174173eqeq1d 2823 . . . . . . . . . 10 (𝑤 = 𝑦 → ({𝑥, 𝑤} = {𝑎, 𝑏} ↔ {𝑥, 𝑦} = {𝑎, 𝑏}))
175174anbi1d 631 . . . . . . . . 9 (𝑤 = 𝑦 → (({𝑥, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ↔ ({𝑥, 𝑦} = {𝑎, 𝑏} ∧ 𝜑)))
1761752exbidv 1925 . . . . . . . 8 (𝑤 = 𝑦 → (∃𝑎∃𝑏({𝑥, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ↔ ∃𝑎∃𝑏({𝑥, 𝑦} = {𝑎, 𝑏} ∧ 𝜑)))
177173eqeq2d 2832 . . . . . . . . . 10 (𝑤 = 𝑦 → ({𝑚, 𝑛} = {𝑥, 𝑤} ↔ {𝑚, 𝑛} = {𝑥, 𝑦}))
178177imbi2d 343 . . . . . . . . 9 (𝑤 = 𝑦 → ((∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑤}) ↔ (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑦})))
1791782ralbidv 3199 . . . . . . . 8 (𝑤 = 𝑦 → (∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑤}) ↔ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑦})))
180176, 179anbi12d 632 . . . . . . 7 (𝑤 = 𝑦 → ((∃𝑎∃𝑏({𝑥, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑤})) ↔ (∃𝑎∃𝑏({𝑥, 𝑦} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑦}))))
181172, 180rspc2ev 3635 . . . . . 6 ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (∃𝑎∃𝑏({𝑥, 𝑦} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑥, 𝑦}))) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑋 (∃𝑎∃𝑏({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑣, 𝑤})))
1828, 9, 15, 164, 181syl112anc 1370 . . . . 5 (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩))) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑋 (∃𝑎∃𝑏({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑣, 𝑤})))
183182ex 415 . . . 4 ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ((∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑋 (∃𝑎∃𝑏({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑣, 𝑤}))))
184183rexlimivv 3292 . . 3 (∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑋 (∃𝑎∃𝑏({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑣, 𝑤})))
185 eqeq1 2825 . . . . . 6 (𝑝 = {𝑣, 𝑤} → (𝑝 = {𝑎, 𝑏} ↔ {𝑣, 𝑤} = {𝑎, 𝑏}))
186185anbi1d 631 . . . . 5 (𝑝 = {𝑣, 𝑤} → ((𝑝 = {𝑎, 𝑏} ∧ 𝜑) ↔ ({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑)))
1871862exbidv 1925 . . . 4 (𝑝 = {𝑣, 𝑤} → (∃𝑎∃𝑏(𝑝 = {𝑎, 𝑏} ∧ 𝜑) ↔ ∃𝑎∃𝑏({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑)))
188 eqeq1 2825 . . . . . 6 (𝑝 = {𝑚, 𝑛} → (𝑝 = {𝑎, 𝑏} ↔ {𝑚, 𝑛} = {𝑎, 𝑏}))
189188anbi1d 631 . . . . 5 (𝑝 = {𝑚, 𝑛} → ((𝑝 = {𝑎, 𝑏} ∧ 𝜑) ↔ ({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑)))
1901892exbidv 1925 . . . 4 (𝑝 = {𝑚, 𝑛} → (∃𝑎∃𝑏(𝑝 = {𝑎, 𝑏} ∧ 𝜑) ↔ ∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑)))
191187, 190reupr 43733 . . 3 (𝑋 ∈ 𝑉 → (∃!𝑝 ∈ (Pairs‘𝑋)∃𝑎∃𝑏(𝑝 = {𝑎, 𝑏} ∧ 𝜑) ↔ ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑋 (∃𝑎∃𝑏({𝑣, 𝑤} = {𝑎, 𝑏} ∧ 𝜑) ∧ ∀𝑚 ∈ 𝑋 ∀𝑛 ∈ 𝑋 (∃𝑎∃𝑏({𝑚, 𝑛} = {𝑎, 𝑏} ∧ 𝜑) → {𝑚, 𝑛} = {𝑣, 𝑤}))))
192184, 191syl5ibr 248 . 2 (𝑋 ∈ 𝑉 → (∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑖 ∈ 𝑋 ∀𝑗 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑖, 𝑗⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑖, 𝑗⟩ = ⟨𝑥, 𝑦⟩)) → ∃!𝑝 ∈ (Pairs‘𝑋)∃𝑎∃𝑏(𝑝 = {𝑎, 𝑏} ∧ 𝜑)))
1937, 192syl5bi 244 1 (𝑋 ∈ 𝑉 → (∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎∃𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ∃!𝑝 ∈ (Pairs‘𝑋)∃𝑎∃𝑏(𝑝 = {𝑎, 𝑏} ∧ 𝜑)))
Colors of variables: wff setvar class
Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 843   ∧ w3a 1083   = wceq 1537  ∃wex 1780   ∈ wcel 2114  ∀wral 3138  ∃wrex 3139  ∃!wreu 3140  Vcvv 3494  [wsbc 3772  {cpr 4569  ⟨cop 4573   × cxp 5553  ‘cfv 6355  Pairscspr 43688
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-rep 5190  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-fal 1550  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-spr 43689
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator