Theorem ichnreuop 47453

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 3790	. . . . . . . . . 10 ⊢ Ⅎ𝑎[𝑐 / 𝑎][𝑑 / 𝑏]𝜑
7	4, 5, 6	nf3an 1901	. . . . . . . . 9 ⊢ Ⅎ𝑎(⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)
8		nfv 1914	. . . . . . . . . 10 ⊢ Ⅎ𝑏⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩
9		nfv 1914	. . . . . . . . . 10 ⊢ Ⅎ𝑏 𝑐 ≠ 𝑑
10		nfcv 2899	. . . . . . . . . . 11 ⊢ Ⅎ𝑏𝑐
11		nfsbc1v 3790	. . . . . . . . . . 11 ⊢ Ⅎ𝑏[𝑑 / 𝑏]𝜑
12	10, 11	nfsbcw 3792	. . . . . . . . . 10 ⊢ Ⅎ𝑏[𝑐 / 𝑎][𝑑 / 𝑏]𝜑
13	8, 9, 12	nf3an 1901	. . . . . . . . 9 ⊢ Ⅎ𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)
14		opeq12 4856	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩)
15	14	eqeq2d 2747	. . . . . . . . . 10 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩))
16		simpl 482	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → 𝑎 = 𝑐)
17		simpr 484	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → 𝑏 = 𝑑)
18	16, 17	neeq12d 2994	. . . . . . . . . 10 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 ≠ 𝑏 ↔ 𝑐 ≠ 𝑑))
19		sbceq1a 3781	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑑 → (𝜑 ↔ [𝑑 / 𝑏]𝜑))
20		sbceq1a 3781	. . . . . . . . . . 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 3468	. . . . . . . . . . . . . . . 16 ⊢ 𝑥 ∈ V
25		vex 3468	. . . . . . . . . . . . . . . 16 ⊢ 𝑦 ∈ V
26	24, 25	opth 5456	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ↔ (𝑥 = 𝑐 ∧ 𝑦 = 𝑑))
27		eleq1w 2818	. . . . . . . . . . . . . . . . . . . 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 1133	. . . . . . . . . . . . 13 ⊢ ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑑 ∈ 𝑋))
35	34	impcom 407	. . . . . . . . . . . 12 ⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → 𝑑 ∈ 𝑋)
36		eleq1w 2818	. . . . . . . . . . . . . . . . . . . 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 1133	. . . . . . . . . . . . 13 ⊢ ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑐 ∈ 𝑋))
44	43	impcom 407	. . . . . . . . . . . 12 ⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → 𝑐 ∈ 𝑋)
45		eqidd 2737	. . . . . . . . . . . . . . . 16 ⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩)
46		necom 2986	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 ≠ 𝑑 ↔ 𝑑 ≠ 𝑐)
47	46	biimpi 216	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ≠ 𝑑 → 𝑑 ≠ 𝑐)
48	47	3ad2ant2 1134	. . . . . . . . . . . . . . . . 17 ⊢ ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → 𝑑 ≠ 𝑐)
49	48	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → 𝑑 ≠ 𝑐)
50		dfich2 47439	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ([𝑎⇄𝑏]𝜑 ↔ ∀𝑐∀𝑑([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
51		2sp 2187	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑐∀𝑑([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑) → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
52		sbsbc 3774	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ([𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑏]𝜑)
53	52	sbbii 2077	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)
54		sbsbc 3774	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)
55	53, 54	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)
56		sbsbc 3774	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ([𝑐 / 𝑏]𝜑 ↔ [𝑐 / 𝑏]𝜑)
57	56	sbbii 2077	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ([𝑑 / 𝑎][𝑐 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑)
58		sbsbc 3774	. . . . . . . . . . . . . . . . . . . . . . . . 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 1135	. . . . . . . . . . . . . . . . . 18 ⊢ ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → [𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
66	65	impcom 407	. . . . . . . . . . . . . . . . 17 ⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → [𝑑 / 𝑎][𝑐 / 𝑏]𝜑)
67		sbccom 3851	. . . . . . . . . . . . . . . . 17 ⊢ ([𝑐 / 𝑏][𝑑 / 𝑎]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑)
68	66, 67	sylibr 234	. . . . . . . . . . . . . . . 16 ⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → [𝑐 / 𝑏][𝑑 / 𝑎]𝜑)
69	45, 49, 68	3jca 1128	. . . . . . . . . . . . . . 15 ⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → (⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩ ∧ 𝑑 ≠ 𝑐 ∧ [𝑐 / 𝑏][𝑑 / 𝑎]𝜑))
70		nfv 1914	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑏⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩
71		nfv 1914	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑏 𝑑 ≠ 𝑐
72		nfsbc1v 3790	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑏[𝑐 / 𝑏][𝑑 / 𝑎]𝜑
73	70, 71, 72	nf3an 1901	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩ ∧ 𝑑 ≠ 𝑐 ∧ [𝑐 / 𝑏][𝑑 / 𝑎]𝜑)
74		opeq2 4855	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝑐 → ⟨𝑑, 𝑏⟩ = ⟨𝑑, 𝑐⟩)
75	74	eqeq2d 2747	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑐 → (⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩))
76		neeq2 2996	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑐 → (𝑑 ≠ 𝑏 ↔ 𝑑 ≠ 𝑐))
77		sbceq1a 3781	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑐 → ([𝑑 / 𝑎]𝜑 ↔ [𝑐 / 𝑏][𝑑 / 𝑎]𝜑))
78	75, 76, 77	3anbi123d 1438	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑐 → ((⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑) ↔ (⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩ ∧ 𝑑 ≠ 𝑐 ∧ [𝑐 / 𝑏][𝑑 / 𝑎]𝜑)))
79	10, 73, 78	spcegf 3576	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ∈ 𝑋 → ((⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩ ∧ 𝑑 ≠ 𝑐 ∧ [𝑐 / 𝑏][𝑑 / 𝑎]𝜑) → ∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑)))
80	44, 69, 79	sylc 65	. . . . . . . . . . . . . 14 ⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑))
81		nfcv 2899	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑎𝑑
82		nfv 1914	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑎⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩
83		nfv 1914	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑎 𝑑 ≠ 𝑏
84		nfsbc1v 3790	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑎[𝑑 / 𝑎]𝜑
85	82, 83, 84	nf3an 1901	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑎(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑)
86	85	nfex 2325	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑎∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑)
87		opeq1 4854	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑑 → ⟨𝑎, 𝑏⟩ = ⟨𝑑, 𝑏⟩)
88	87	eqeq2d 2747	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑑 → (⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩))
89		neeq1 2995	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑑 → (𝑎 ≠ 𝑏 ↔ 𝑑 ≠ 𝑏))
90		sbceq1a 3781	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑑 → (𝜑 ↔ [𝑑 / 𝑎]𝜑))
91	88, 89, 90	3anbi123d 1438	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑑 → ((⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ (⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑)))
92	91	exbidv 1921	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑑 → (∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ ∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑)))
93	81, 86, 92	spcegf 3576	. . . . . . . . . . . . . 14 ⊢ (𝑑 ∈ 𝑋 → (∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑) → ∃𝑎∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)))
94	35, 80, 93	sylc 65	. . . . . . . . . . . . 13 ⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ∃𝑎∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑))
95		vex 3468	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑑 ∈ V
96		vex 3468	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑐 ∈ V
97	95, 96	opth1 5455	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩ → 𝑑 = 𝑐)
98	97	equcomd 2019	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩ → 𝑐 = 𝑑)
99	98	necon3ai 2958	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 ≠ 𝑑 → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩)
100	99	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑) → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩)
101		eqeq2 2748	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ → (⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩))
102	101	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑) → (⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩))
103	100, 102	mtbird 325	. . . . . . . . . . . . . . 15 ⊢ ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑) → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)
104	103	3adant3 1132	. . . . . . . . . . . . . 14 ⊢ ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)
105	104	adantl 481	. . . . . . . . . . . . 13 ⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)
106	94, 105	jcnd 163	. . . . . . . . . . . 12 ⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ¬ (∃𝑎∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩))
107		opeq1 4854	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = 𝑑 → ⟨𝑣, 𝑤⟩ = ⟨𝑑, 𝑤⟩)
108	107	eqeq1d 2738	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑑 → (⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩))
109	108	3anbi1d 1442	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑑 → ((⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ (⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)))
110	109	2exbidv 1924	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑑 → (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ ∃𝑎∃𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)))
111	107	eqeq1d 2738	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑑 → (⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
112	110, 111	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑑 → ((∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ (∃𝑎∃𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
113	112	notbid 318	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑑 → (¬ (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ ¬ (∃𝑎∃𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
114		opeq2 4855	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑐 → ⟨𝑑, 𝑤⟩ = ⟨𝑑, 𝑐⟩)
115	114	eqeq1d 2738	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑐 → (⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩))
116	115	3anbi1d 1442	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑐 → ((⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ (⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)))
117	116	2exbidv 1924	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑐 → (∃𝑎∃𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ ∃𝑎∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)))
118	114	eqeq1d 2738	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑐 → (⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩))
119	117, 118	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑐 → ((∃𝑎∃𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ (∃𝑎∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)))
120	119	notbid 318	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑐 → (¬ (∃𝑎∃𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ ¬ (∃𝑎∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)))
121	113, 120	rspc2ev 3619	. . . . . . . . . . . 12 ⊢ ((𝑑 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ∧ ¬ (∃𝑎∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑋 ¬ (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
122	35, 44, 106, 121	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑋 ¬ (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
123		rexnal2 3123	. . . . . . . . . . 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 863	. . . . 5 ⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (¬ ∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∨ ¬ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
130		ianor 983	. . . . 5 ⊢ (¬ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∧ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)) ↔ (¬ ∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∨ ¬ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
131	129, 130	sylibr 234	. . . 4 ⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ¬ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∧ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
132	131	ralrimivva 3188	. . 3 ⊢ ([𝑎⇄𝑏]𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ¬ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∧ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
133		ralnex2 3121	. . 3 ⊢ (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ¬ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∧ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)) ↔ ¬ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∧ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
134	132, 133	sylib 218	. 2 ⊢ ([𝑎⇄𝑏]𝜑 → ¬ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∧ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
135		eqeq1 2740	. . . . 5 ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (𝑝 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))
136	135	3anbi1d 1442	. . . 4 ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → ((𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)))
137	136	2exbidv 1924	. . 3 ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (∃𝑎∃𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ ∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)))
138		eqeq1 2740	. . . . 5 ⊢ (𝑝 = ⟨𝑣, 𝑤⟩ → (𝑝 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩))
139	138	3anbi1d 1442	. . . 4 ⊢ (𝑝 = ⟨𝑣, 𝑤⟩ → ((𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ (⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)))
140	139	2exbidv 1924	. . 3 ⊢ (𝑝 = ⟨𝑣, 𝑤⟩ → (∃𝑎∃𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ ∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)))
141	137, 140	reuop 6287	. 2 ⊢ (∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎∃𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∧ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
142	134, 141	sylnibr 329	1 ⊢ ([𝑎⇄𝑏]𝜑 → ¬ ∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎∃𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086  ∀wal 1538   = wceq 1540  ∃wex 1779  [wsb 2065   ∈ wcel 2109   ≠ wne 2933  ∀wral 3052  ∃wrex 3061  ∃!wreu 3362  [wsbc 3770  ⟨cop 4612   × cxp 5657  [wich 47426

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rmo 3364  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-opab 5187  df-xp 5665  df-ich 47427

This theorem is referenced by: (None)