Theorem ichnreuop 47459

Description: If the setvar variables are interchangeable in a wff, there is never a unique ordered pair with different components fulfilling the wff (because if ⟨𝑎, 𝑏⟩ fulfils the wff, then also ⟨𝑏, 𝑎⟩ fulfils the wff). (Contributed by AV, 27-Aug-2023.)

Assertion

Ref	Expression
ichnreuop	⊢ ([𝑎⇄𝑏]𝜑 → ¬ ∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎∃𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑))

Distinct variable groups:   𝑎,𝑏,𝑝   𝜑,𝑝   𝑋,𝑝

Allowed substitution hints:   𝜑(𝑎,𝑏)   𝑋(𝑎,𝑏)

Proof of Theorem ichnreuop

Dummy variables 𝑐 𝑑 𝑣 𝑤 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		notnotb 315	. . . . . . 7 ⊢ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ ¬ ¬ ∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑))
2		nfv 1914	. . . . . . . . 9 ⊢ Ⅎ𝑐(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)
3		nfv 1914	. . . . . . . . 9 ⊢ Ⅎ𝑑(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)
4		nfv 1914	. . . . . . . . . 10 ⊢ Ⅎ𝑎⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩
5		nfv 1914	. . . . . . . . . 10 ⊢ Ⅎ𝑎 𝑐 ≠ 𝑑
6		nfsbc1v 3808	. . . . . . . . . 10 ⊢ Ⅎ𝑎[𝑐 / 𝑎][𝑑 / 𝑏]𝜑
7	4, 5, 6	nf3an 1901	. . . . . . . . 9 ⊢ Ⅎ𝑎(⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)
8		nfv 1914	. . . . . . . . . 10 ⊢ Ⅎ𝑏⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩
9		nfv 1914	. . . . . . . . . 10 ⊢ Ⅎ𝑏 𝑐 ≠ 𝑑
10		nfcv 2905	. . . . . . . . . . 11 ⊢ Ⅎ𝑏𝑐
11		nfsbc1v 3808	. . . . . . . . . . 11 ⊢ Ⅎ𝑏[𝑑 / 𝑏]𝜑
12	10, 11	nfsbcw 3810	. . . . . . . . . 10 ⊢ Ⅎ𝑏[𝑐 / 𝑎][𝑑 / 𝑏]𝜑
13	8, 9, 12	nf3an 1901	. . . . . . . . 9 ⊢ Ⅎ𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)
14		opeq12 4875	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩)
15	14	eqeq2d 2748	. . . . . . . . . 10 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩))
16		simpl 482	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → 𝑎 = 𝑐)
17		simpr 484	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → 𝑏 = 𝑑)
18	16, 17	neeq12d 3002	. . . . . . . . . 10 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 ≠ 𝑏 ↔ 𝑐 ≠ 𝑑))
19		sbceq1a 3799	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑑 → (𝜑 ↔ [𝑑 / 𝑏]𝜑))
20		sbceq1a 3799	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑐 → ([𝑑 / 𝑏]𝜑 ↔ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑))
21	19, 20	sylan9bbr 510	. . . . . . . . . 10 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝜑 ↔ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑))
22	15, 18, 21	3anbi123d 1438	. . . . . . . . 9 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → ((⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)))
23	2, 3, 7, 13, 22	cbvex2v 2346	. . . . . . . 8 ⊢ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ ∃𝑐∃𝑑(⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑))
24		vex 3484	. . . . . . . . . . . . . . . 16 ⊢ 𝑥 ∈ V
25		vex 3484	. . . . . . . . . . . . . . . 16 ⊢ 𝑦 ∈ V
26	24, 25	opth 5481	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ↔ (𝑥 = 𝑐 ∧ 𝑦 = 𝑑))
27		eleq1w 2824	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑑 → (𝑦 ∈ 𝑋 ↔ 𝑑 ∈ 𝑋))
28	27	biimpcd 249	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ 𝑋 → (𝑦 = 𝑑 → 𝑑 ∈ 𝑋))
29	28	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑦 = 𝑑 → 𝑑 ∈ 𝑋))
30	29	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑦 = 𝑑 → 𝑑 ∈ 𝑋))
31	30	com12 32	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑑 → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑑 ∈ 𝑋))
32	31	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = 𝑐 ∧ 𝑦 = 𝑑) → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑑 ∈ 𝑋))
33	26, 32	sylbi 217	. . . . . . . . . . . . . 14 ⊢ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑑 ∈ 𝑋))
34	33	3ad2ant1 1134	. . . . . . . . . . . . 13 ⊢ ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑑 ∈ 𝑋))
35	34	impcom 407	. . . . . . . . . . . 12 ⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → 𝑑 ∈ 𝑋)
36		eleq1w 2824	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑐 → (𝑥 ∈ 𝑋 ↔ 𝑐 ∈ 𝑋))
37	36	biimpcd 249	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝑋 → (𝑥 = 𝑐 → 𝑐 ∈ 𝑋))
38	37	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥 = 𝑐 → 𝑐 ∈ 𝑋))
39	38	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥 = 𝑐 → 𝑐 ∈ 𝑋))
40	39	com12 32	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑐 → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑐 ∈ 𝑋))
41	40	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = 𝑐 ∧ 𝑦 = 𝑑) → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑐 ∈ 𝑋))
42	26, 41	sylbi 217	. . . . . . . . . . . . . 14 ⊢ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑐 ∈ 𝑋))
43	42	3ad2ant1 1134	. . . . . . . . . . . . 13 ⊢ ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑐 ∈ 𝑋))
44	43	impcom 407	. . . . . . . . . . . 12 ⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → 𝑐 ∈ 𝑋)
45		eqidd 2738	. . . . . . . . . . . . . . . 16 ⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩)
46		necom 2994	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 ≠ 𝑑 ↔ 𝑑 ≠ 𝑐)
47	46	biimpi 216	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ≠ 𝑑 → 𝑑 ≠ 𝑐)
48	47	3ad2ant2 1135	. . . . . . . . . . . . . . . . 17 ⊢ ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → 𝑑 ≠ 𝑐)
49	48	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → 𝑑 ≠ 𝑐)
50		dfich2 47445	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ([𝑎⇄𝑏]𝜑 ↔ ∀𝑐∀𝑑([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
51		2sp 2186	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑐∀𝑑([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑) → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
52		sbsbc 3792	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ([𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑏]𝜑)
53	52	sbbii 2076	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)
54		sbsbc 3792	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)
55	53, 54	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)
56		sbsbc 3792	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ([𝑐 / 𝑏]𝜑 ↔ [𝑐 / 𝑏]𝜑)
57	56	sbbii 2076	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ([𝑑 / 𝑎][𝑐 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑)
58		sbsbc 3792	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ([𝑑 / 𝑎][𝑐 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑)
59	57, 58	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ([𝑑 / 𝑎][𝑐 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑)
60	51, 55, 59	3bitr3g 313	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∀𝑐∀𝑑([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑) → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
61	60	biimpd 229	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑐∀𝑑([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑) → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 → [𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
62	50, 61	sylbi 217	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ([𝑎⇄𝑏]𝜑 → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 → [𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
63	62	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 → [𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
64	63	com12 32	. . . . . . . . . . . . . . . . . . 19 ⊢ ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → [𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
65	64	3ad2ant3 1136	. . . . . . . . . . . . . . . . . 18 ⊢ ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → [𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
66	65	impcom 407	. . . . . . . . . . . . . . . . 17 ⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → [𝑑 / 𝑎][𝑐 / 𝑏]𝜑)
67		sbccom 3871	. . . . . . . . . . . . . . . . 17 ⊢ ([𝑐 / 𝑏][𝑑 / 𝑎]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑)
68	66, 67	sylibr 234	. . . . . . . . . . . . . . . 16 ⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → [𝑐 / 𝑏][𝑑 / 𝑎]𝜑)
69	45, 49, 68	3jca 1129	. . . . . . . . . . . . . . 15 ⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → (⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩ ∧ 𝑑 ≠ 𝑐 ∧ [𝑐 / 𝑏][𝑑 / 𝑎]𝜑))
70		nfv 1914	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑏⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩
71		nfv 1914	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑏 𝑑 ≠ 𝑐
72		nfsbc1v 3808	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑏[𝑐 / 𝑏][𝑑 / 𝑎]𝜑
73	70, 71, 72	nf3an 1901	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩ ∧ 𝑑 ≠ 𝑐 ∧ [𝑐 / 𝑏][𝑑 / 𝑎]𝜑)
74		opeq2 4874	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝑐 → ⟨𝑑, 𝑏⟩ = ⟨𝑑, 𝑐⟩)
75	74	eqeq2d 2748	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑐 → (⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩))
76		neeq2 3004	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑐 → (𝑑 ≠ 𝑏 ↔ 𝑑 ≠ 𝑐))
77		sbceq1a 3799	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑐 → ([𝑑 / 𝑎]𝜑 ↔ [𝑐 / 𝑏][𝑑 / 𝑎]𝜑))
78	75, 76, 77	3anbi123d 1438	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑐 → ((⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑) ↔ (⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩ ∧ 𝑑 ≠ 𝑐 ∧ [𝑐 / 𝑏][𝑑 / 𝑎]𝜑)))
79	10, 73, 78	spcegf 3592	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ∈ 𝑋 → ((⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩ ∧ 𝑑 ≠ 𝑐 ∧ [𝑐 / 𝑏][𝑑 / 𝑎]𝜑) → ∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑)))
80	44, 69, 79	sylc 65	. . . . . . . . . . . . . 14 ⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑))
81		nfcv 2905	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑎𝑑
82		nfv 1914	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑎⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩
83		nfv 1914	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑎 𝑑 ≠ 𝑏
84		nfsbc1v 3808	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑎[𝑑 / 𝑎]𝜑
85	82, 83, 84	nf3an 1901	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑎(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑)
86	85	nfex 2324	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑎∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑)
87		opeq1 4873	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑑 → ⟨𝑎, 𝑏⟩ = ⟨𝑑, 𝑏⟩)
88	87	eqeq2d 2748	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑑 → (⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩))
89		neeq1 3003	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑑 → (𝑎 ≠ 𝑏 ↔ 𝑑 ≠ 𝑏))
90		sbceq1a 3799	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑑 → (𝜑 ↔ [𝑑 / 𝑎]𝜑))
91	88, 89, 90	3anbi123d 1438	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑑 → ((⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ (⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑)))
92	91	exbidv 1921	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑑 → (∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ ∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑)))
93	81, 86, 92	spcegf 3592	. . . . . . . . . . . . . 14 ⊢ (𝑑 ∈ 𝑋 → (∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑) → ∃𝑎∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)))
94	35, 80, 93	sylc 65	. . . . . . . . . . . . 13 ⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ∃𝑎∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑))
95		vex 3484	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑑 ∈ V
96		vex 3484	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑐 ∈ V
97	95, 96	opth1 5480	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩ → 𝑑 = 𝑐)
98	97	equcomd 2018	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩ → 𝑐 = 𝑑)
99	98	necon3ai 2965	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 ≠ 𝑑 → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩)
100	99	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑) → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩)
101		eqeq2 2749	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ → (⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩))
102	101	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑) → (⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩))
103	100, 102	mtbird 325	. . . . . . . . . . . . . . 15 ⊢ ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑) → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)
104	103	3adant3 1133	. . . . . . . . . . . . . 14 ⊢ ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)
105	104	adantl 481	. . . . . . . . . . . . 13 ⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)
106	94, 105	jcnd 163	. . . . . . . . . . . 12 ⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ¬ (∃𝑎∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩))
107		opeq1 4873	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = 𝑑 → ⟨𝑣, 𝑤⟩ = ⟨𝑑, 𝑤⟩)
108	107	eqeq1d 2739	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑑 → (⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩))
109	108	3anbi1d 1442	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑑 → ((⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ (⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)))
110	109	2exbidv 1924	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑑 → (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ ∃𝑎∃𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)))
111	107	eqeq1d 2739	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑑 → (⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
112	110, 111	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑑 → ((∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ (∃𝑎∃𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
113	112	notbid 318	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑑 → (¬ (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ ¬ (∃𝑎∃𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
114		opeq2 4874	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑐 → ⟨𝑑, 𝑤⟩ = ⟨𝑑, 𝑐⟩)
115	114	eqeq1d 2739	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑐 → (⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩))
116	115	3anbi1d 1442	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑐 → ((⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ (⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)))
117	116	2exbidv 1924	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑐 → (∃𝑎∃𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ ∃𝑎∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)))
118	114	eqeq1d 2739	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑐 → (⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩))
119	117, 118	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑐 → ((∃𝑎∃𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ (∃𝑎∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)))
120	119	notbid 318	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑐 → (¬ (∃𝑎∃𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ ¬ (∃𝑎∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)))
121	113, 120	rspc2ev 3635	. . . . . . . . . . . 12 ⊢ ((𝑑 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ∧ ¬ (∃𝑎∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑋 ¬ (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
122	35, 44, 106, 121	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑋 ¬ (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
123		rexnal2 3135	. . . . . . . . . . 11 ⊢ (∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑋 ¬ (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ ¬ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
124	122, 123	sylib 218	. . . . . . . . . 10 ⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ¬ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
125	124	ex 412	. . . . . . . . 9 ⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → ¬ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
126	125	exlimdvv 1934	. . . . . . . 8 ⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (∃𝑐∃𝑑(⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → ¬ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
127	23, 126	biimtrid 242	. . . . . . 7 ⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ¬ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
128	1, 127	biimtrrid 243	. . . . . 6 ⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (¬ ¬ ∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ¬ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
129	128	orrd 864	. . . . 5 ⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (¬ ∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∨ ¬ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
130		ianor 984	. . . . 5 ⊢ (¬ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∧ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)) ↔ (¬ ∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∨ ¬ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
131	129, 130	sylibr 234	. . . 4 ⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ¬ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∧ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
132	131	ralrimivva 3202	. . 3 ⊢ ([𝑎⇄𝑏]𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ¬ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∧ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
133		ralnex2 3133	. . 3 ⊢ (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ¬ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∧ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)) ↔ ¬ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∧ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
134	132, 133	sylib 218	. 2 ⊢ ([𝑎⇄𝑏]𝜑 → ¬ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∧ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
135		eqeq1 2741	. . . . 5 ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (𝑝 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))
136	135	3anbi1d 1442	. . . 4 ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → ((𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)))
137	136	2exbidv 1924	. . 3 ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (∃𝑎∃𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ ∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)))
138		eqeq1 2741	. . . . 5 ⊢ (𝑝 = ⟨𝑣, 𝑤⟩ → (𝑝 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩))
139	138	3anbi1d 1442	. . . 4 ⊢ (𝑝 = ⟨𝑣, 𝑤⟩ → ((𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ (⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)))
140	139	2exbidv 1924	. . 3 ⊢ (𝑝 = ⟨𝑣, 𝑤⟩ → (∃𝑎∃𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ ∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)))
141	137, 140	reuop 6313	. 2 ⊢ (∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎∃𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∧ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
142	134, 141	sylnibr 329	1 ⊢ ([𝑎⇄𝑏]𝜑 → ¬ ∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎∃𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∧ w3a 1087  ∀wal 1538   = wceq 1540  ∃wex 1779  [wsb 2064   ∈ wcel 2108   ≠ wne 2940  ∀wral 3061  ∃wrex 3070  ∃!wreu 3378  [wsbc 3788  ⟨cop 4632   × cxp 5683  [wich 47432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-opab 5206  df-xp 5691  df-ich 47433

This theorem is referenced by: (None)