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 44051
 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 2802 . . . . 5 (𝑝 = ⟨𝑥, 𝑦⟩ → (𝑝 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))
21anbi1d 632 . . . 4 (𝑝 = ⟨𝑥, 𝑦⟩ → ((𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
322exbidv 1925 . . 3 (𝑝 = ⟨𝑥, 𝑦⟩ → (∃𝑎𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
4 eqeq1 2802 . . . . 5 (𝑝 = ⟨𝑣, 𝑤⟩ → (𝑝 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩))
54anbi1d 632 . . . 4 (𝑝 = ⟨𝑣, 𝑤⟩ → ((𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
652exbidv 1925 . . 3 (𝑝 = ⟨𝑣, 𝑤⟩ → (∃𝑎𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
73, 6reuop 6115 . 2 (∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑥𝑋𝑦𝑋 (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
8 nfich1 44025 . . . . . 6 𝑎[𝑎𝑏]𝜑
9 nfv 1915 . . . . . 6 𝑎(𝑥𝑋𝑦𝑋)
108, 9nfan 1900 . . . . 5 𝑎([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋))
11 nfcv 2955 . . . . . . 7 𝑎𝑋
12 nfe1 2151 . . . . . . . . 9 𝑎𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)
13 nfv 1915 . . . . . . . . 9 𝑎𝑣, 𝑤⟩ = ⟨𝑥, 𝑦
1412, 13nfim 1897 . . . . . . . 8 𝑎(∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)
1511, 14nfralw 3189 . . . . . . 7 𝑎𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)
1611, 15nfralw 3189 . . . . . 6 𝑎𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)
17 nfe1 2151 . . . . . 6 𝑎𝑎𝑏(𝑎 = 𝑏𝜑)
1816, 17nfim 1897 . . . . 5 𝑎(∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) → ∃𝑎𝑏(𝑎 = 𝑏𝜑))
19 nfich2 44026 . . . . . . 7 𝑏[𝑎𝑏]𝜑
20 nfv 1915 . . . . . . 7 𝑏(𝑥𝑋𝑦𝑋)
2119, 20nfan 1900 . . . . . 6 𝑏([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋))
22 nfcv 2955 . . . . . . . 8 𝑏𝑋
23 nfe1 2151 . . . . . . . . . . 11 𝑏𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)
2423nfex 2332 . . . . . . . . . 10 𝑏𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)
25 nfv 1915 . . . . . . . . . 10 𝑏𝑣, 𝑤⟩ = ⟨𝑥, 𝑦
2624, 25nfim 1897 . . . . . . . . 9 𝑏(∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)
2722, 26nfralw 3189 . . . . . . . 8 𝑏𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)
2822, 27nfralw 3189 . . . . . . 7 𝑏𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)
29 nfe1 2151 . . . . . . . 8 𝑏𝑏(𝑎 = 𝑏𝜑)
3029nfex 2332 . . . . . . 7 𝑏𝑎𝑏(𝑎 = 𝑏𝜑)
3128, 30nfim 1897 . . . . . 6 𝑏(∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) → ∃𝑎𝑏(𝑎 = 𝑏𝜑))
32 opeq12 4768 . . . . . . . . . . . . . 14 ((𝑣 = 𝑦𝑤 = 𝑥) → ⟨𝑣, 𝑤⟩ = ⟨𝑦, 𝑥⟩)
3332eqeq1d 2800 . . . . . . . . . . . . 13 ((𝑣 = 𝑦𝑤 = 𝑥) → (⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑦, 𝑥⟩ = ⟨𝑎, 𝑏⟩))
3433anbi1d 632 . . . . . . . . . . . 12 ((𝑣 = 𝑦𝑤 = 𝑥) → ((⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑦, 𝑥⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
35342exbidv 1925 . . . . . . . . . . 11 ((𝑣 = 𝑦𝑤 = 𝑥) → (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑎𝑏(⟨𝑦, 𝑥⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
3632eqeq1d 2800 . . . . . . . . . . 11 ((𝑣 = 𝑦𝑤 = 𝑥) → (⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑦, 𝑥⟩ = ⟨𝑥, 𝑦⟩))
3735, 36imbi12d 348 . . . . . . . . . 10 ((𝑣 = 𝑦𝑤 = 𝑥) → ((∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ (∃𝑎𝑏(⟨𝑦, 𝑥⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑦, 𝑥⟩ = ⟨𝑥, 𝑦⟩)))
3837rspc2gv 3580 . . . . . . . . 9 ((𝑦𝑋𝑥𝑋) → (∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) → (∃𝑎𝑏(⟨𝑦, 𝑥⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑦, 𝑥⟩ = ⟨𝑥, 𝑦⟩)))
3938ancoms 462 . . . . . . . 8 ((𝑥𝑋𝑦𝑋) → (∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) → (∃𝑎𝑏(⟨𝑦, 𝑥⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑦, 𝑥⟩ = ⟨𝑥, 𝑦⟩)))
4039adantl 485 . . . . . . 7 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) → (∃𝑎𝑏(⟨𝑦, 𝑥⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑦, 𝑥⟩ = ⟨𝑥, 𝑦⟩)))
41 simprr 772 . . . . . . . . . . 11 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑦𝑋)
4241adantr 484 . . . . . . . . . 10 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)) → 𝑦𝑋)
43 simpl 486 . . . . . . . . . . . . 13 ((𝑥𝑋𝑦𝑋) → 𝑥𝑋)
4443adantl 485 . . . . . . . . . . . 12 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑥𝑋)
4544adantr 484 . . . . . . . . . . 11 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)) → 𝑥𝑋)
46 eqidd 2799 . . . . . . . . . . . 12 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)) → ⟨𝑦, 𝑥⟩ = ⟨𝑦, 𝑥⟩)
47 vex 3444 . . . . . . . . . . . . . . . . 17 𝑥 ∈ V
48 vex 3444 . . . . . . . . . . . . . . . . 17 𝑦 ∈ V
4947, 48opth 5334 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ↔ (𝑥 = 𝑎𝑦 = 𝑏))
50 sbceq1a 3731 . . . . . . . . . . . . . . . . . . 19 (𝑏 = 𝑦 → (𝜑[𝑦 / 𝑏]𝜑))
5150equcoms 2027 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑏 → (𝜑[𝑦 / 𝑏]𝜑))
52 sbceq1a 3731 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑥 → ([𝑦 / 𝑏]𝜑[𝑥 / 𝑎][𝑦 / 𝑏]𝜑))
5352equcoms 2027 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑎 → ([𝑦 / 𝑏]𝜑[𝑥 / 𝑎][𝑦 / 𝑏]𝜑))
5451, 53sylan9bbr 514 . . . . . . . . . . . . . . . . 17 ((𝑥 = 𝑎𝑦 = 𝑏) → (𝜑[𝑥 / 𝑎][𝑦 / 𝑏]𝜑))
55 dfich2 44036 . . . . . . . . . . . . . . . . . . . . 21 ([𝑎𝑏]𝜑 ↔ ∀𝑥𝑦([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜑))
56 2sp 2183 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑥𝑦([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜑) → ([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜑))
57 sbsbc 3724 . . . . . . . . . . . . . . . . . . . . . . . 24 ([𝑦 / 𝑏]𝜑[𝑦 / 𝑏]𝜑)
5857sbbii 2081 . . . . . . . . . . . . . . . . . . . . . . 23 ([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ↔ [𝑥 / 𝑎][𝑦 / 𝑏]𝜑)
59 sbsbc 3724 . . . . . . . . . . . . . . . . . . . . . . 23 ([𝑥 / 𝑎][𝑦 / 𝑏]𝜑[𝑥 / 𝑎][𝑦 / 𝑏]𝜑)
6058, 59bitri 278 . . . . . . . . . . . . . . . . . . . . . 22 ([𝑥 / 𝑎][𝑦 / 𝑏]𝜑[𝑥 / 𝑎][𝑦 / 𝑏]𝜑)
61 sbsbc 3724 . . . . . . . . . . . . . . . . . . . . . . . 24 ([𝑥 / 𝑏]𝜑[𝑥 / 𝑏]𝜑)
6261sbbii 2081 . . . . . . . . . . . . . . . . . . . . . . 23 ([𝑦 / 𝑎][𝑥 / 𝑏]𝜑 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜑)
63 sbsbc 3724 . . . . . . . . . . . . . . . . . . . . . . 23 ([𝑦 / 𝑎][𝑥 / 𝑏]𝜑[𝑦 / 𝑎][𝑥 / 𝑏]𝜑)
6462, 63bitri 278 . . . . . . . . . . . . . . . . . . . . . 22 ([𝑦 / 𝑎][𝑥 / 𝑏]𝜑[𝑦 / 𝑎][𝑥 / 𝑏]𝜑)
6556, 60, 643bitr3g 316 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑥𝑦([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 ↔ [𝑦 / 𝑎][𝑥 / 𝑏]𝜑) → ([𝑥 / 𝑎][𝑦 / 𝑏]𝜑[𝑦 / 𝑎][𝑥 / 𝑏]𝜑))
6655, 65sylbi 220 . . . . . . . . . . . . . . . . . . . 20 ([𝑎𝑏]𝜑 → ([𝑥 / 𝑎][𝑦 / 𝑏]𝜑[𝑦 / 𝑎][𝑥 / 𝑏]𝜑))
6766biimpd 232 . . . . . . . . . . . . . . . . . . 19 ([𝑎𝑏]𝜑 → ([𝑥 / 𝑎][𝑦 / 𝑏]𝜑[𝑦 / 𝑎][𝑥 / 𝑏]𝜑))
6867adantr 484 . . . . . . . . . . . . . . . . . 18 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → ([𝑥 / 𝑎][𝑦 / 𝑏]𝜑[𝑦 / 𝑎][𝑥 / 𝑏]𝜑))
6968com12 32 . . . . . . . . . . . . . . . . 17 ([𝑥 / 𝑎][𝑦 / 𝑏]𝜑 → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → [𝑦 / 𝑎][𝑥 / 𝑏]𝜑))
7054, 69syl6bi 256 . . . . . . . . . . . . . . . 16 ((𝑥 = 𝑎𝑦 = 𝑏) → (𝜑 → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → [𝑦 / 𝑎][𝑥 / 𝑏]𝜑)))
7149, 70sylbi 220 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ → (𝜑 → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → [𝑦 / 𝑎][𝑥 / 𝑏]𝜑)))
7271imp 410 . . . . . . . . . . . . . 14 ((⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → [𝑦 / 𝑎][𝑥 / 𝑏]𝜑))
7372impcom 411 . . . . . . . . . . . . 13 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)) → [𝑦 / 𝑎][𝑥 / 𝑏]𝜑)
74 sbccom 3800 . . . . . . . . . . . . 13 ([𝑥 / 𝑏][𝑦 / 𝑎]𝜑[𝑦 / 𝑎][𝑥 / 𝑏]𝜑)
7573, 74sylibr 237 . . . . . . . . . . . 12 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)) → [𝑥 / 𝑏][𝑦 / 𝑎]𝜑)
7646, 75jca 515 . . . . . . . . . . 11 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)) → (⟨𝑦, 𝑥⟩ = ⟨𝑦, 𝑥⟩ ∧ [𝑥 / 𝑏][𝑦 / 𝑎]𝜑))
77 nfcv 2955 . . . . . . . . . . . 12 𝑏𝑥
78 nfv 1915 . . . . . . . . . . . . 13 𝑏𝑦, 𝑥⟩ = ⟨𝑦, 𝑥
79 nfsbc1v 3740 . . . . . . . . . . . . 13 𝑏[𝑥 / 𝑏][𝑦 / 𝑎]𝜑
8078, 79nfan 1900 . . . . . . . . . . . 12 𝑏(⟨𝑦, 𝑥⟩ = ⟨𝑦, 𝑥⟩ ∧ [𝑥 / 𝑏][𝑦 / 𝑎]𝜑)
81 opeq2 4766 . . . . . . . . . . . . . 14 (𝑏 = 𝑥 → ⟨𝑦, 𝑏⟩ = ⟨𝑦, 𝑥⟩)
8281eqeq2d 2809 . . . . . . . . . . . . 13 (𝑏 = 𝑥 → (⟨𝑦, 𝑥⟩ = ⟨𝑦, 𝑏⟩ ↔ ⟨𝑦, 𝑥⟩ = ⟨𝑦, 𝑥⟩))
83 sbceq1a 3731 . . . . . . . . . . . . 13 (𝑏 = 𝑥 → ([𝑦 / 𝑎]𝜑[𝑥 / 𝑏][𝑦 / 𝑎]𝜑))
8482, 83anbi12d 633 . . . . . . . . . . . 12 (𝑏 = 𝑥 → ((⟨𝑦, 𝑥⟩ = ⟨𝑦, 𝑏⟩ ∧ [𝑦 / 𝑎]𝜑) ↔ (⟨𝑦, 𝑥⟩ = ⟨𝑦, 𝑥⟩ ∧ [𝑥 / 𝑏][𝑦 / 𝑎]𝜑)))
8577, 80, 84spcegf 3539 . . . . . . . . . . 11 (𝑥𝑋 → ((⟨𝑦, 𝑥⟩ = ⟨𝑦, 𝑥⟩ ∧ [𝑥 / 𝑏][𝑦 / 𝑎]𝜑) → ∃𝑏(⟨𝑦, 𝑥⟩ = ⟨𝑦, 𝑏⟩ ∧ [𝑦 / 𝑎]𝜑)))
8645, 76, 85sylc 65 . . . . . . . . . 10 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)) → ∃𝑏(⟨𝑦, 𝑥⟩ = ⟨𝑦, 𝑏⟩ ∧ [𝑦 / 𝑎]𝜑))
87 nfcv 2955 . . . . . . . . . . 11 𝑎𝑦
88 nfv 1915 . . . . . . . . . . . . 13 𝑎𝑦, 𝑥⟩ = ⟨𝑦, 𝑏
89 nfsbc1v 3740 . . . . . . . . . . . . 13 𝑎[𝑦 / 𝑎]𝜑
9088, 89nfan 1900 . . . . . . . . . . . 12 𝑎(⟨𝑦, 𝑥⟩ = ⟨𝑦, 𝑏⟩ ∧ [𝑦 / 𝑎]𝜑)
9190nfex 2332 . . . . . . . . . . 11 𝑎𝑏(⟨𝑦, 𝑥⟩ = ⟨𝑦, 𝑏⟩ ∧ [𝑦 / 𝑎]𝜑)
92 opeq1 4764 . . . . . . . . . . . . . 14 (𝑎 = 𝑦 → ⟨𝑎, 𝑏⟩ = ⟨𝑦, 𝑏⟩)
9392eqeq2d 2809 . . . . . . . . . . . . 13 (𝑎 = 𝑦 → (⟨𝑦, 𝑥⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑦, 𝑥⟩ = ⟨𝑦, 𝑏⟩))
94 sbceq1a 3731 . . . . . . . . . . . . 13 (𝑎 = 𝑦 → (𝜑[𝑦 / 𝑎]𝜑))
9593, 94anbi12d 633 . . . . . . . . . . . 12 (𝑎 = 𝑦 → ((⟨𝑦, 𝑥⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ (⟨𝑦, 𝑥⟩ = ⟨𝑦, 𝑏⟩ ∧ [𝑦 / 𝑎]𝜑)))
9695exbidv 1922 . . . . . . . . . . 11 (𝑎 = 𝑦 → (∃𝑏(⟨𝑦, 𝑥⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑏(⟨𝑦, 𝑥⟩ = ⟨𝑦, 𝑏⟩ ∧ [𝑦 / 𝑎]𝜑)))
9787, 91, 96spcegf 3539 . . . . . . . . . 10 (𝑦𝑋 → (∃𝑏(⟨𝑦, 𝑥⟩ = ⟨𝑦, 𝑏⟩ ∧ [𝑦 / 𝑎]𝜑) → ∃𝑎𝑏(⟨𝑦, 𝑥⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
9842, 86, 97sylc 65 . . . . . . . . 9 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)) → ∃𝑎𝑏(⟨𝑦, 𝑥⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑))
99 simpl 486 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 = 𝑥 ∧ (𝑥 = 𝑎𝑦 = 𝑏)) → 𝑦 = 𝑥)
100 simprr 772 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 = 𝑥 ∧ (𝑥 = 𝑎𝑦 = 𝑏)) → 𝑦 = 𝑏)
101 simpl 486 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 = 𝑎𝑦 = 𝑏) → 𝑥 = 𝑎)
102101adantl 485 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 = 𝑥 ∧ (𝑥 = 𝑎𝑦 = 𝑏)) → 𝑥 = 𝑎)
10399, 100, 1023eqtr3rd 2842 . . . . . . . . . . . . . . . . . . 19 ((𝑦 = 𝑥 ∧ (𝑥 = 𝑎𝑦 = 𝑏)) → 𝑎 = 𝑏)
104103anim1i 617 . . . . . . . . . . . . . . . . . 18 (((𝑦 = 𝑥 ∧ (𝑥 = 𝑎𝑦 = 𝑏)) ∧ 𝜑) → (𝑎 = 𝑏𝜑))
105104exp31 423 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑥 → ((𝑥 = 𝑎𝑦 = 𝑏) → (𝜑 → (𝑎 = 𝑏𝜑))))
10649, 105syl5bi 245 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑥 → (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ → (𝜑 → (𝑎 = 𝑏𝜑))))
107106impd 414 . . . . . . . . . . . . . . 15 (𝑦 = 𝑥 → ((⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → (𝑎 = 𝑏𝜑)))
10848, 47opth1 5333 . . . . . . . . . . . . . . 15 (⟨𝑦, 𝑥⟩ = ⟨𝑥, 𝑦⟩ → 𝑦 = 𝑥)
109107, 108syl11 33 . . . . . . . . . . . . . 14 ((⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → (⟨𝑦, 𝑥⟩ = ⟨𝑥, 𝑦⟩ → (𝑎 = 𝑏𝜑)))
110109adantl 485 . . . . . . . . . . . . 13 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)) → (⟨𝑦, 𝑥⟩ = ⟨𝑥, 𝑦⟩ → (𝑎 = 𝑏𝜑)))
111110imp 410 . . . . . . . . . . . 12 (((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)) ∧ ⟨𝑦, 𝑥⟩ = ⟨𝑥, 𝑦⟩) → (𝑎 = 𝑏𝜑))
11211119.8ad 2179 . . . . . . . . . . 11 (((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)) ∧ ⟨𝑦, 𝑥⟩ = ⟨𝑥, 𝑦⟩) → ∃𝑏(𝑎 = 𝑏𝜑))
11311219.8ad 2179 . . . . . . . . . 10 (((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)) ∧ ⟨𝑦, 𝑥⟩ = ⟨𝑥, 𝑦⟩) → ∃𝑎𝑏(𝑎 = 𝑏𝜑))
114113ex 416 . . . . . . . . 9 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)) → (⟨𝑦, 𝑥⟩ = ⟨𝑥, 𝑦⟩ → ∃𝑎𝑏(𝑎 = 𝑏𝜑)))
11598, 114embantd 59 . . . . . . . 8 ((([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)) → ((∃𝑎𝑏(⟨𝑦, 𝑥⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑦, 𝑥⟩ = ⟨𝑥, 𝑦⟩) → ∃𝑎𝑏(𝑎 = 𝑏𝜑)))
116115ex 416 . . . . . . 7 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → ((⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ((∃𝑎𝑏(⟨𝑦, 𝑥⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑦, 𝑥⟩ = ⟨𝑥, 𝑦⟩) → ∃𝑎𝑏(𝑎 = 𝑏𝜑))))
11740, 116syl5d 73 . . . . . 6 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → ((⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → (∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) → ∃𝑎𝑏(𝑎 = 𝑏𝜑))))
11821, 31, 117exlimd 2216 . . . . 5 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → (∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) → ∃𝑎𝑏(𝑎 = 𝑏𝜑))))
11910, 18, 118exlimd 2216 . . . 4 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → (∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) → ∃𝑎𝑏(𝑎 = 𝑏𝜑))))
120119impd 414 . . 3 (([𝑎𝑏]𝜑 ∧ (𝑥𝑋𝑦𝑋)) → ((∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)) → ∃𝑎𝑏(𝑎 = 𝑏𝜑)))
121120rexlimdvva 3253 . 2 ([𝑎𝑏]𝜑 → (∃𝑥𝑋𝑦𝑋 (∃𝑎𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ∧ ∀𝑣𝑋𝑤𝑋 (∃𝑎𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)) → ∃𝑎𝑏(𝑎 = 𝑏𝜑)))
1227, 121syl5bi 245 1 ([𝑎𝑏]𝜑 → (∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ∃𝑎𝑏(𝑎 = 𝑏𝜑)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1536   = wceq 1538  ∃wex 1781  [wsb 2069   ∈ wcel 2111  ∀wral 3106  ∃wrex 3107  ∃!wreu 3108  [wsbc 3720  ⟨cop 4531   × cxp 5518  [wich 44023 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5168  ax-nul 5175  ax-pr 5296 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-opab 5094  df-xp 5526  df-ich 44024 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator