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

Theorem ichreuopeq 45265
Description: If the setvar variables are interchangeable in a wff, and there is a unique ordered pair fulfilling the wff, then both setvar variables must be equal. (Contributed by AV, 28-Aug-2023.)
Assertion
Ref Expression
ichreuopeq ([𝑎𝑏]𝜑 → (∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ∃𝑎𝑏(𝑎 = 𝑏𝜑)))
Distinct variable groups:   𝑋,𝑎,𝑏,𝑝   𝜑,𝑝
Allowed substitution hints:   𝜑(𝑎,𝑏)

Proof of Theorem ichreuopeq
Dummy variables 𝑣 𝑤 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqeq1 2740 . . . . 5 (𝑝 = ⟨𝑥, 𝑦⟩ → (𝑝 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))
21anbi1d 630 . . . 4 (𝑝 = ⟨𝑥, 𝑦⟩ → ((𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
322exbidv 1926 . . 3 (𝑝 = ⟨𝑥, 𝑦⟩ → (∃𝑎𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
4 eqeq1 2740 . . . . 5 (𝑝 = ⟨𝑣, 𝑤⟩ → (𝑝 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩))
54anbi1d 630 . . . 4 (𝑝 = ⟨𝑣, 𝑤⟩ → ((𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
652exbidv 1926 . . 3 (𝑝 = ⟨𝑣, 𝑤⟩ → (∃𝑎𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
73, 6reuop 6225 . 2 (∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑥𝑋𝑦𝑋 (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
8 nfich1 45239 . . . . . 6 𝑎[𝑎𝑏]𝜑
9 nfv 1916 . . . . . 6 𝑎(𝑥𝑋𝑦𝑋)
108, 9nfan 1901 . . . . 5 𝑎([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋))
11 nfcv 2904 . . . . . . 7 𝑎𝑋
12 nfe1 2146 . . . . . . . . 9 𝑎𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)
13 nfv 1916 . . . . . . . . 9 𝑎𝑣, 𝑤⟩ = ⟨𝑥, 𝑦
1412, 13nfim 1898 . . . . . . . 8 𝑎(∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)
1511, 14nfralw 3290 . . . . . . 7 𝑎𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)
1611, 15nfralw 3290 . . . . . 6 𝑎𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)
17 nfe1 2146 . . . . . 6 𝑎𝑎𝑏(𝑎 = 𝑏𝜑)
1816, 17nfim 1898 . . . . 5 𝑎(∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) → ∃𝑎𝑏(𝑎 = 𝑏𝜑))
19 nfich2 45240 . . . . . . 7 𝑏[𝑎𝑏]𝜑
20 nfv 1916 . . . . . . 7 𝑏(𝑥𝑋𝑦𝑋)
2119, 20nfan 1901 . . . . . 6 𝑏([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋))
22 nfcv 2904 . . . . . . . 8 𝑏𝑋
23 nfe1 2146 . . . . . . . . . . 11 𝑏𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)
2423nfex 2317 . . . . . . . . . 10 𝑏𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)
25 nfv 1916 . . . . . . . . . 10 𝑏𝑣, 𝑤⟩ = ⟨𝑥, 𝑦
2624, 25nfim 1898 . . . . . . . . 9 𝑏(∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)
2722, 26nfralw 3290 . . . . . . . 8 𝑏𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)
2822, 27nfralw 3290 . . . . . . 7 𝑏𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)
29 nfe1 2146 . . . . . . . 8 𝑏𝑏(𝑎 = 𝑏𝜑)
3029nfex 2317 . . . . . . 7 𝑏𝑎𝑏(𝑎 = 𝑏𝜑)
3128, 30nfim 1898 . . . . . 6 𝑏(∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) → ∃𝑎𝑏(𝑎 = 𝑏𝜑))
32 opeq12 4818 . . . . . . . . . . . . . 14 ((𝑣 = 𝑦𝑤 = 𝑥) → ⟨𝑣, 𝑤⟩ = ⟨𝑦, 𝑥⟩)
3332eqeq1d 2738 . . . . . . . . . . . . 13 ((𝑣 = 𝑦𝑤 = 𝑥) → (⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑦, 𝑥⟩ = ⟨𝑎, 𝑏⟩))
3433anbi1d 630 . . . . . . . . . . . 12 ((𝑣 = 𝑦𝑤 = 𝑥) → ((⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑦, 𝑥⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
35342exbidv 1926 . . . . . . . . . . 11 ((𝑣 = 𝑦𝑤 = 𝑥) → (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑎𝑏(⟨𝑦, 𝑥⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
3632eqeq1d 2738 . . . . . . . . . . 11 ((𝑣 = 𝑦𝑤 = 𝑥) → (⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑦, 𝑥⟩ = ⟨𝑥, 𝑦⟩))
3735, 36imbi12d 344 . . . . . . . . . 10 ((𝑣 = 𝑦𝑤 = 𝑥) → ((∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ (∃𝑎𝑏(⟨𝑦, 𝑥⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑦, 𝑥⟩ = ⟨𝑥, 𝑦⟩)))
3837rspc2gv 3578 . . . . . . . . 9 ((𝑦𝑋𝑥𝑋) → (∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) → (∃𝑎𝑏(⟨𝑦, 𝑥⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑦, 𝑥⟩ = ⟨𝑥, 𝑦⟩)))
3938ancoms 459 . . . . . . . 8 ((𝑥𝑋𝑦𝑋) → (∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) → (∃𝑎𝑏(⟨𝑦, 𝑥⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑦, 𝑥⟩ = ⟨𝑥, 𝑦⟩)))
4039adantl 482 . . . . . . 7 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) → (∃𝑎𝑏(⟨𝑦, 𝑥⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑦, 𝑥⟩ = ⟨𝑥, 𝑦⟩)))
41 simprr 770 . . . . . . . . . . 11 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑦𝑋)
4241adantr 481 . . . . . . . . . 10 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)) → 𝑦𝑋)
43 simpl 483 . . . . . . . . . . . . 13 ((𝑥𝑋𝑦𝑋) → 𝑥𝑋)
4443adantl 482 . . . . . . . . . . . 12 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑥𝑋)
4544adantr 481 . . . . . . . . . . 11 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)) → 𝑥𝑋)
46 eqidd 2737 . . . . . . . . . . . 12 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)) → ⟨𝑦, 𝑥⟩ = ⟨𝑦, 𝑥⟩)
47 vex 3445 . . . . . . . . . . . . . . . . 17 𝑥 ∈ V
48 vex 3445 . . . . . . . . . . . . . . . . 17 𝑦 ∈ V
4947, 48opth 5415 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ↔ (𝑥 = 𝑎𝑦 = 𝑏))
50 sbceq1a 3737 . . . . . . . . . . . . . . . . . . 19 (𝑏 = 𝑦 → (𝜑[𝑦 / 𝑏]𝜑))
5150equcoms 2022 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑏 → (𝜑[𝑦 / 𝑏]𝜑))
52 sbceq1a 3737 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑥 → ([𝑦 / 𝑏]𝜑[𝑥 / 𝑎][𝑦 / 𝑏]𝜑))
5352equcoms 2022 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑎 → ([𝑦 / 𝑏]𝜑[𝑥 / 𝑎][𝑦 / 𝑏]𝜑))
5451, 53sylan9bbr 511 . . . . . . . . . . . . . . . . 17 ((𝑥 = 𝑎𝑦 = 𝑏) → (𝜑[𝑥 / 𝑎][𝑦 / 𝑏]𝜑))
55 dfich2 45250 . . . . . . . . . . . . . . . . . . . . 21 ([𝑎𝑏]𝜑 ↔ ∀𝑥𝑦([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜑))
56 2sp 2178 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑥𝑦([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜑) → ([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜑))
57 sbsbc 3730 . . . . . . . . . . . . . . . . . . . . . . . 24 ([𝑦 / 𝑏]𝜑[𝑦 / 𝑏]𝜑)
5857sbbii 2078 . . . . . . . . . . . . . . . . . . . . . . 23 ([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ↔ [𝑥 / 𝑎][𝑦 / 𝑏]𝜑)
59 sbsbc 3730 . . . . . . . . . . . . . . . . . . . . . . 23 ([𝑥 / 𝑎][𝑦 / 𝑏]𝜑[𝑥 / 𝑎][𝑦 / 𝑏]𝜑)
6058, 59bitri 274 . . . . . . . . . . . . . . . . . . . . . 22 ([𝑥 / 𝑎][𝑦 / 𝑏]𝜑[𝑥 / 𝑎][𝑦 / 𝑏]𝜑)
61 sbsbc 3730 . . . . . . . . . . . . . . . . . . . . . . . 24 ([𝑥 / 𝑏]𝜑[𝑥 / 𝑏]𝜑)
6261sbbii 2078 . . . . . . . . . . . . . . . . . . . . . . 23 ([𝑦 / 𝑎][𝑥 / 𝑏]𝜑 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜑)
63 sbsbc 3730 . . . . . . . . . . . . . . . . . . . . . . 23 ([𝑦 / 𝑎][𝑥 / 𝑏]𝜑[𝑦 / 𝑎][𝑥 / 𝑏]𝜑)
6462, 63bitri 274 . . . . . . . . . . . . . . . . . . . . . 22 ([𝑦 / 𝑎][𝑥 / 𝑏]𝜑[𝑦 / 𝑎][𝑥 / 𝑏]𝜑)
6556, 60, 643bitr3g 312 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑥𝑦([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜑) → ([𝑥 / 𝑎][𝑦 / 𝑏]𝜑[𝑦 / 𝑎][𝑥 / 𝑏]𝜑))
6655, 65sylbi 216 . . . . . . . . . . . . . . . . . . . 20 ([𝑎𝑏]𝜑 → ([𝑥 / 𝑎][𝑦 / 𝑏]𝜑[𝑦 / 𝑎][𝑥 / 𝑏]𝜑))
6766biimpd 228 . . . . . . . . . . . . . . . . . . 19 ([𝑎𝑏]𝜑 → ([𝑥 / 𝑎][𝑦 / 𝑏]𝜑[𝑦 / 𝑎][𝑥 / 𝑏]𝜑))
6867adantr 481 . . . . . . . . . . . . . . . . . 18 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → ([𝑥 / 𝑎][𝑦 / 𝑏]𝜑[𝑦 / 𝑎][𝑥 / 𝑏]𝜑))
6968com12 32 . . . . . . . . . . . . . . . . 17 ([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → [𝑦 / 𝑎][𝑥 / 𝑏]𝜑))
7054, 69syl6bi 252 . . . . . . . . . . . . . . . 16 ((𝑥 = 𝑎𝑦 = 𝑏) → (𝜑 → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → [𝑦 / 𝑎][𝑥 / 𝑏]𝜑)))
7149, 70sylbi 216 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ → (𝜑 → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → [𝑦 / 𝑎][𝑥 / 𝑏]𝜑)))
7271imp 407 . . . . . . . . . . . . . 14 ((⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → [𝑦 / 𝑎][𝑥 / 𝑏]𝜑))
7372impcom 408 . . . . . . . . . . . . 13 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)) → [𝑦 / 𝑎][𝑥 / 𝑏]𝜑)
74 sbccom 3814 . . . . . . . . . . . . 13 ([𝑥 / 𝑏][𝑦 / 𝑎]𝜑[𝑦 / 𝑎][𝑥 / 𝑏]𝜑)
7573, 74sylibr 233 . . . . . . . . . . . 12 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)) → [𝑥 / 𝑏][𝑦 / 𝑎]𝜑)
7646, 75jca 512 . . . . . . . . . . 11 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)) → (⟨𝑦, 𝑥⟩ = ⟨𝑦, 𝑥⟩ ∧ [𝑥 / 𝑏][𝑦 / 𝑎]𝜑))
77 nfcv 2904 . . . . . . . . . . . 12 𝑏𝑥
78 nfv 1916 . . . . . . . . . . . . 13 𝑏𝑦, 𝑥⟩ = ⟨𝑦, 𝑥
79 nfsbc1v 3746 . . . . . . . . . . . . 13 𝑏[𝑥 / 𝑏][𝑦 / 𝑎]𝜑
8078, 79nfan 1901 . . . . . . . . . . . 12 𝑏(⟨𝑦, 𝑥⟩ = ⟨𝑦, 𝑥⟩ ∧ [𝑥 / 𝑏][𝑦 / 𝑎]𝜑)
81 opeq2 4817 . . . . . . . . . . . . . 14 (𝑏 = 𝑥 → ⟨𝑦, 𝑏⟩ = ⟨𝑦, 𝑥⟩)
8281eqeq2d 2747 . . . . . . . . . . . . 13 (𝑏 = 𝑥 → (⟨𝑦, 𝑥⟩ = ⟨𝑦, 𝑏⟩ ↔ ⟨𝑦, 𝑥⟩ = ⟨𝑦, 𝑥⟩))
83 sbceq1a 3737 . . . . . . . . . . . . 13 (𝑏 = 𝑥 → ([𝑦 / 𝑎]𝜑[𝑥 / 𝑏][𝑦 / 𝑎]𝜑))
8482, 83anbi12d 631 . . . . . . . . . . . 12 (𝑏 = 𝑥 → ((⟨𝑦, 𝑥⟩ = ⟨𝑦, 𝑏⟩ ∧ [𝑦 / 𝑎]𝜑) ↔ (⟨𝑦, 𝑥⟩ = ⟨𝑦, 𝑥⟩ ∧ [𝑥 / 𝑏][𝑦 / 𝑎]𝜑)))
8577, 80, 84spcegf 3540 . . . . . . . . . . 11 (𝑥𝑋 → ((⟨𝑦, 𝑥⟩ = ⟨𝑦, 𝑥⟩ ∧ [𝑥 / 𝑏][𝑦 / 𝑎]𝜑) → ∃𝑏(⟨𝑦, 𝑥⟩ = ⟨𝑦, 𝑏⟩ ∧ [𝑦 / 𝑎]𝜑)))
8645, 76, 85sylc 65 . . . . . . . . . 10 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)) → ∃𝑏(⟨𝑦, 𝑥⟩ = ⟨𝑦, 𝑏⟩ ∧ [𝑦 / 𝑎]𝜑))
87 nfcv 2904 . . . . . . . . . . 11 𝑎𝑦
88 nfv 1916 . . . . . . . . . . . . 13 𝑎𝑦, 𝑥⟩ = ⟨𝑦, 𝑏
89 nfsbc1v 3746 . . . . . . . . . . . . 13 𝑎[𝑦 / 𝑎]𝜑
9088, 89nfan 1901 . . . . . . . . . . . 12 𝑎(⟨𝑦, 𝑥⟩ = ⟨𝑦, 𝑏⟩ ∧ [𝑦 / 𝑎]𝜑)
9190nfex 2317 . . . . . . . . . . 11 𝑎𝑏(⟨𝑦, 𝑥⟩ = ⟨𝑦, 𝑏⟩ ∧ [𝑦 / 𝑎]𝜑)
92 opeq1 4816 . . . . . . . . . . . . . 14 (𝑎 = 𝑦 → ⟨𝑎, 𝑏⟩ = ⟨𝑦, 𝑏⟩)
9392eqeq2d 2747 . . . . . . . . . . . . 13 (𝑎 = 𝑦 → (⟨𝑦, 𝑥⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑦, 𝑥⟩ = ⟨𝑦, 𝑏⟩))
94 sbceq1a 3737 . . . . . . . . . . . . 13 (𝑎 = 𝑦 → (𝜑[𝑦 / 𝑎]𝜑))
9593, 94anbi12d 631 . . . . . . . . . . . 12 (𝑎 = 𝑦 → ((⟨𝑦, 𝑥⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑦, 𝑥⟩ = ⟨𝑦, 𝑏⟩ ∧ [𝑦 / 𝑎]𝜑)))
9695exbidv 1923 . . . . . . . . . . 11 (𝑎 = 𝑦 → (∃𝑏(⟨𝑦, 𝑥⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑏(⟨𝑦, 𝑥⟩ = ⟨𝑦, 𝑏⟩ ∧ [𝑦 / 𝑎]𝜑)))
9787, 91, 96spcegf 3540 . . . . . . . . . 10 (𝑦𝑋 → (∃𝑏(⟨𝑦, 𝑥⟩ = ⟨𝑦, 𝑏⟩ ∧ [𝑦 / 𝑎]𝜑) → ∃𝑎𝑏(⟨𝑦, 𝑥⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
9842, 86, 97sylc 65 . . . . . . . . 9 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)) → ∃𝑎𝑏(⟨𝑦, 𝑥⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑))
99 simpl 483 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 = 𝑥 ∧ (𝑥 = 𝑎𝑦 = 𝑏)) → 𝑦 = 𝑥)
100 simprr 770 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 = 𝑥 ∧ (𝑥 = 𝑎𝑦 = 𝑏)) → 𝑦 = 𝑏)
101 simpl 483 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 = 𝑎𝑦 = 𝑏) → 𝑥 = 𝑎)
102101adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 = 𝑥 ∧ (𝑥 = 𝑎𝑦 = 𝑏)) → 𝑥 = 𝑎)
10399, 100, 1023eqtr3rd 2785 . . . . . . . . . . . . . . . . . . 19 ((𝑦 = 𝑥 ∧ (𝑥 = 𝑎𝑦 = 𝑏)) → 𝑎 = 𝑏)
104103anim1i 615 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 𝑥 ∧ (𝑥 = 𝑎𝑦 = 𝑏)) ∧ 𝜑) → (𝑎 = 𝑏𝜑))
105104exp31 420 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑥 → ((𝑥 = 𝑎𝑦 = 𝑏) → (𝜑 → (𝑎 = 𝑏𝜑))))
10649, 105biimtrid 241 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑥 → (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ → (𝜑 → (𝑎 = 𝑏𝜑))))
107106impd 411 . . . . . . . . . . . . . . 15 (𝑦 = 𝑥 → ((⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → (𝑎 = 𝑏𝜑)))
10848, 47opth1 5414 . . . . . . . . . . . . . . 15 (⟨𝑦, 𝑥⟩ = ⟨𝑥, 𝑦⟩ → 𝑦 = 𝑥)
109107, 108syl11 33 . . . . . . . . . . . . . 14 ((⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → (⟨𝑦, 𝑥⟩ = ⟨𝑥, 𝑦⟩ → (𝑎 = 𝑏𝜑)))
110109adantl 482 . . . . . . . . . . . . 13 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)) → (⟨𝑦, 𝑥⟩ = ⟨𝑥, 𝑦⟩ → (𝑎 = 𝑏𝜑)))
111110imp 407 . . . . . . . . . . . 12 (((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)) ∧ ⟨𝑦, 𝑥⟩ = ⟨𝑥, 𝑦⟩) → (𝑎 = 𝑏𝜑))
11211119.8ad 2174 . . . . . . . . . . 11 (((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)) ∧ ⟨𝑦, 𝑥⟩ = ⟨𝑥, 𝑦⟩) → ∃𝑏(𝑎 = 𝑏𝜑))
11311219.8ad 2174 . . . . . . . . . 10 (((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)) ∧ ⟨𝑦, 𝑥⟩ = ⟨𝑥, 𝑦⟩) → ∃𝑎𝑏(𝑎 = 𝑏𝜑))
114113ex 413 . . . . . . . . 9 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)) → (⟨𝑦, 𝑥⟩ = ⟨𝑥, 𝑦⟩ → ∃𝑎𝑏(𝑎 = 𝑏𝜑)))
11598, 114embantd 59 . . . . . . . 8 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)) → ((∃𝑎𝑏(⟨𝑦, 𝑥⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑦, 𝑥⟩ = ⟨𝑥, 𝑦⟩) → ∃𝑎𝑏(𝑎 = 𝑏𝜑)))
116115ex 413 . . . . . . 7 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → ((⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ((∃𝑎𝑏(⟨𝑦, 𝑥⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑦, 𝑥⟩ = ⟨𝑥, 𝑦⟩) → ∃𝑎𝑏(𝑎 = 𝑏𝜑))))
11740, 116syl5d 73 . . . . . 6 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → ((⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → (∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) → ∃𝑎𝑏(𝑎 = 𝑏𝜑))))
11821, 31, 117exlimd 2210 . . . . 5 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → (∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) → ∃𝑎𝑏(𝑎 = 𝑏𝜑))))
11910, 18, 118exlimd 2210 . . . 4 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → (∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) → ∃𝑎𝑏(𝑎 = 𝑏𝜑))))
120119impd 411 . . 3 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → ((∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)) → ∃𝑎𝑏(𝑎 = 𝑏𝜑)))
121120rexlimdvva 3201 . 2 ([𝑎𝑏]𝜑 → (∃𝑥𝑋𝑦𝑋 (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)) → ∃𝑎𝑏(𝑎 = 𝑏𝜑)))
1227, 121biimtrid 241 1 ([𝑎𝑏]𝜑 → (∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ∃𝑎𝑏(𝑎 = 𝑏𝜑)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wal 1538   = wceq 1540  wex 1780  [wsb 2066  wcel 2105  wral 3061  wrex 3070  ∃!wreu 3347  [wsbc 3726  cop 4578   × cxp 5612  [wich 45237
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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5240  ax-nul 5247  ax-pr 5369
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4269  df-if 4473  df-sn 4573  df-pr 4575  df-op 4579  df-opab 5152  df-xp 5620  df-ich 45238
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator