Theorem ichnreuop 44924

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 1917	. . . . . . . . 9 ⊢ Ⅎ𝑐(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)
3		nfv 1917	. . . . . . . . 9 ⊢ Ⅎ𝑑(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)
4		nfv 1917	. . . . . . . . . 10 ⊢ Ⅎ𝑎⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩
5		nfv 1917	. . . . . . . . . 10 ⊢ Ⅎ𝑎 𝑐 ≠ 𝑑
6		nfsbc1v 3736	. . . . . . . . . 10 ⊢ Ⅎ𝑎[𝑐 / 𝑎][𝑑 / 𝑏]𝜑
7	4, 5, 6	nf3an 1904	. . . . . . . . 9 ⊢ Ⅎ𝑎(⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)
8		nfv 1917	. . . . . . . . . 10 ⊢ Ⅎ𝑏⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩
9		nfv 1917	. . . . . . . . . 10 ⊢ Ⅎ𝑏 𝑐 ≠ 𝑑
10		nfcv 2907	. . . . . . . . . . 11 ⊢ Ⅎ𝑏𝑐
11		nfsbc1v 3736	. . . . . . . . . . 11 ⊢ Ⅎ𝑏[𝑑 / 𝑏]𝜑
12	10, 11	nfsbcw 3738	. . . . . . . . . 10 ⊢ Ⅎ𝑏[𝑐 / 𝑎][𝑑 / 𝑏]𝜑
13	8, 9, 12	nf3an 1904	. . . . . . . . 9 ⊢ Ⅎ𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)
14		opeq12 4806	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩)
15	14	eqeq2d 2749	. . . . . . . . . 10 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩))
16		simpl 483	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → 𝑎 = 𝑐)
17		simpr 485	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → 𝑏 = 𝑑)
18	16, 17	neeq12d 3005	. . . . . . . . . 10 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 ≠ 𝑏 ↔ 𝑐 ≠ 𝑑))
19		sbceq1a 3727	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑑 → (𝜑 ↔ [𝑑 / 𝑏]𝜑))
20		sbceq1a 3727	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑐 → ([𝑑 / 𝑏]𝜑 ↔ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑))
21	19, 20	sylan9bbr 511	. . . . . . . . . 10 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝜑 ↔ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑))
22	15, 18, 21	3anbi123d 1435	. . . . . . . . 9 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → ((⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)))
23	2, 3, 7, 13, 22	cbvex2v 2342	. . . . . . . 8 ⊢ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ ∃𝑐∃𝑑(⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑))
24		vex 3436	. . . . . . . . . . . . . . . 16 ⊢ 𝑥 ∈ V
25		vex 3436	. . . . . . . . . . . . . . . 16 ⊢ 𝑦 ∈ V
26	24, 25	opth 5391	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ↔ (𝑥 = 𝑐 ∧ 𝑦 = 𝑑))
27		eleq1w 2821	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑑 → (𝑦 ∈ 𝑋 ↔ 𝑑 ∈ 𝑋))
28	27	biimpcd 248	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ 𝑋 → (𝑦 = 𝑑 → 𝑑 ∈ 𝑋))
29	28	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑦 = 𝑑 → 𝑑 ∈ 𝑋))
30	29	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑦 = 𝑑 → 𝑑 ∈ 𝑋))
31	30	com12 32	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑑 → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑑 ∈ 𝑋))
32	31	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = 𝑐 ∧ 𝑦 = 𝑑) → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑑 ∈ 𝑋))
33	26, 32	sylbi 216	. . . . . . . . . . . . . 14 ⊢ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑑 ∈ 𝑋))
34	33	3ad2ant1 1132	. . . . . . . . . . . . 13 ⊢ ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑑 ∈ 𝑋))
35	34	impcom 408	. . . . . . . . . . . 12 ⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → 𝑑 ∈ 𝑋)
36		eleq1w 2821	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑐 → (𝑥 ∈ 𝑋 ↔ 𝑐 ∈ 𝑋))
37	36	biimpcd 248	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝑋 → (𝑥 = 𝑐 → 𝑐 ∈ 𝑋))
38	37	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥 = 𝑐 → 𝑐 ∈ 𝑋))
39	38	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥 = 𝑐 → 𝑐 ∈ 𝑋))
40	39	com12 32	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑐 → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑐 ∈ 𝑋))
41	40	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = 𝑐 ∧ 𝑦 = 𝑑) → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑐 ∈ 𝑋))
42	26, 41	sylbi 216	. . . . . . . . . . . . . 14 ⊢ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑐 ∈ 𝑋))
43	42	3ad2ant1 1132	. . . . . . . . . . . . 13 ⊢ ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑐 ∈ 𝑋))
44	43	impcom 408	. . . . . . . . . . . 12 ⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → 𝑐 ∈ 𝑋)
45		eqidd 2739	. . . . . . . . . . . . . . . 16 ⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩)
46		necom 2997	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 ≠ 𝑑 ↔ 𝑑 ≠ 𝑐)
47	46	biimpi 215	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ≠ 𝑑 → 𝑑 ≠ 𝑐)
48	47	3ad2ant2 1133	. . . . . . . . . . . . . . . . 17 ⊢ ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → 𝑑 ≠ 𝑐)
49	48	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → 𝑑 ≠ 𝑐)
50		dfich2 44910	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ([𝑎⇄𝑏]𝜑 ↔ ∀𝑐∀𝑑([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
51		2sp 2179	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑐∀𝑑([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑) → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
52		sbsbc 3720	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ([𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑏]𝜑)
53	52	sbbii 2079	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)
54		sbsbc 3720	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)
55	53, 54	bitri 274	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)
56		sbsbc 3720	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ([𝑐 / 𝑏]𝜑 ↔ [𝑐 / 𝑏]𝜑)
57	56	sbbii 2079	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ([𝑑 / 𝑎][𝑐 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑)
58		sbsbc 3720	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ([𝑑 / 𝑎][𝑐 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑)
59	57, 58	bitri 274	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ([𝑑 / 𝑎][𝑐 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑)
60	51, 55, 59	3bitr3g 313	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∀𝑐∀𝑑([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑) → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
61	60	biimpd 228	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑐∀𝑑([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑) → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 → [𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
62	50, 61	sylbi 216	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ([𝑎⇄𝑏]𝜑 → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 → [𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
63	62	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 → [𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
64	63	com12 32	. . . . . . . . . . . . . . . . . . 19 ⊢ ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → [𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
65	64	3ad2ant3 1134	. . . . . . . . . . . . . . . . . 18 ⊢ ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → [𝑑 / 𝑎][𝑐 / 𝑏]𝜑))
66	65	impcom 408	. . . . . . . . . . . . . . . . 17 ⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → [𝑑 / 𝑎][𝑐 / 𝑏]𝜑)
67		sbccom 3804	. . . . . . . . . . . . . . . . 17 ⊢ ([𝑐 / 𝑏][𝑑 / 𝑎]𝜑 ↔ [𝑑 / 𝑎][𝑐 / 𝑏]𝜑)
68	66, 67	sylibr 233	. . . . . . . . . . . . . . . 16 ⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → [𝑐 / 𝑏][𝑑 / 𝑎]𝜑)
69	45, 49, 68	3jca 1127	. . . . . . . . . . . . . . 15 ⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → (⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩ ∧ 𝑑 ≠ 𝑐 ∧ [𝑐 / 𝑏][𝑑 / 𝑎]𝜑))
70		nfv 1917	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑏⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩
71		nfv 1917	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑏 𝑑 ≠ 𝑐
72		nfsbc1v 3736	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑏[𝑐 / 𝑏][𝑑 / 𝑎]𝜑
73	70, 71, 72	nf3an 1904	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩ ∧ 𝑑 ≠ 𝑐 ∧ [𝑐 / 𝑏][𝑑 / 𝑎]𝜑)
74		opeq2 4805	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 𝑐 → ⟨𝑑, 𝑏⟩ = ⟨𝑑, 𝑐⟩)
75	74	eqeq2d 2749	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑐 → (⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩))
76		neeq2 3007	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑐 → (𝑑 ≠ 𝑏 ↔ 𝑑 ≠ 𝑐))
77		sbceq1a 3727	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑐 → ([𝑑 / 𝑎]𝜑 ↔ [𝑐 / 𝑏][𝑑 / 𝑎]𝜑))
78	75, 76, 77	3anbi123d 1435	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑐 → ((⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑) ↔ (⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩ ∧ 𝑑 ≠ 𝑐 ∧ [𝑐 / 𝑏][𝑑 / 𝑎]𝜑)))
79	10, 73, 78	spcegf 3531	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ∈ 𝑋 → ((⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑐⟩ ∧ 𝑑 ≠ 𝑐 ∧ [𝑐 / 𝑏][𝑑 / 𝑎]𝜑) → ∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑)))
80	44, 69, 79	sylc 65	. . . . . . . . . . . . . 14 ⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑))
81		nfcv 2907	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑎𝑑
82		nfv 1917	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑎⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩
83		nfv 1917	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑎 𝑑 ≠ 𝑏
84		nfsbc1v 3736	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑎[𝑑 / 𝑎]𝜑
85	82, 83, 84	nf3an 1904	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑎(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑)
86	85	nfex 2318	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑎∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑)
87		opeq1 4804	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑑 → ⟨𝑎, 𝑏⟩ = ⟨𝑑, 𝑏⟩)
88	87	eqeq2d 2749	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑑 → (⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩))
89		neeq1 3006	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑑 → (𝑎 ≠ 𝑏 ↔ 𝑑 ≠ 𝑏))
90		sbceq1a 3727	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑑 → (𝜑 ↔ [𝑑 / 𝑎]𝜑))
91	88, 89, 90	3anbi123d 1435	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑑 → ((⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ (⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑)))
92	91	exbidv 1924	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑑 → (∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ ∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑)))
93	81, 86, 92	spcegf 3531	. . . . . . . . . . . . . 14 ⊢ (𝑑 ∈ 𝑋 → (∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑑, 𝑏⟩ ∧ 𝑑 ≠ 𝑏 ∧ [𝑑 / 𝑎]𝜑) → ∃𝑎∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)))
94	35, 80, 93	sylc 65	. . . . . . . . . . . . 13 ⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ∃𝑎∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑))
95		vex 3436	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑑 ∈ V
96		vex 3436	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑐 ∈ V
97	95, 96	opth1 5390	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩ → 𝑑 = 𝑐)
98	97	equcomd 2022	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩ → 𝑐 = 𝑑)
99	98	necon3ai 2968	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 ≠ 𝑑 → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩)
100	99	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑) → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩)
101		eqeq2 2750	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ → (⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩))
102	101	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑) → (⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑐, 𝑑⟩))
103	100, 102	mtbird 325	. . . . . . . . . . . . . . 15 ⊢ ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑) → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)
104	103	3adant3 1131	. . . . . . . . . . . . . 14 ⊢ ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)
105	104	adantl 482	. . . . . . . . . . . . 13 ⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ¬ ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)
106	94, 105	jcnd 163	. . . . . . . . . . . 12 ⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ¬ (∃𝑎∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩))
107		opeq1 4804	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 = 𝑑 → ⟨𝑣, 𝑤⟩ = ⟨𝑑, 𝑤⟩)
108	107	eqeq1d 2740	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑑 → (⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩))
109	108	3anbi1d 1439	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑑 → ((⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ (⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)))
110	109	2exbidv 1927	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑑 → (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ ∃𝑎∃𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)))
111	107	eqeq1d 2740	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑑 → (⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
112	110, 111	imbi12d 345	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑑 → ((∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ (∃𝑎∃𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
113	112	notbid 318	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑑 → (¬ (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ ¬ (∃𝑎∃𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
114		opeq2 4805	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑐 → ⟨𝑑, 𝑤⟩ = ⟨𝑑, 𝑐⟩)
115	114	eqeq1d 2740	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑐 → (⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩))
116	115	3anbi1d 1439	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑐 → ((⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ (⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)))
117	116	2exbidv 1927	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑐 → (∃𝑎∃𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ ∃𝑎∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)))
118	114	eqeq1d 2740	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑐 → (⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩))
119	117, 118	imbi12d 345	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑐 → ((∃𝑎∃𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ (∃𝑎∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)))
120	119	notbid 318	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑐 → (¬ (∃𝑎∃𝑏(⟨𝑑, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑑, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ ¬ (∃𝑎∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)))
121	113, 120	rspc2ev 3572	. . . . . . . . . . . 12 ⊢ ((𝑑 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ∧ ¬ (∃𝑎∃𝑏(⟨𝑑, 𝑐⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑑, 𝑐⟩ = ⟨𝑥, 𝑦⟩)) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑋 ¬ (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
122	35, 44, 106, 121	syl3anc 1370	. . . . . . . . . . 11 ⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑋 ¬ (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
123		rexnal2 3187	. . . . . . . . . . 11 ⊢ (∃𝑣 ∈ 𝑋 ∃𝑤 ∈ 𝑋 ¬ (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩) ↔ ¬ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
124	122, 123	sylib 217	. . . . . . . . . 10 ⊢ ((([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) ∧ (⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) → ¬ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩))
125	124	ex 413	. . . . . . . . 9 ⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → ¬ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
126	125	exlimdvv 1937	. . . . . . . 8 ⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (∃𝑐∃𝑑(⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝑐 ≠ 𝑑 ∧ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑) → ¬ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
127	23, 126	syl5bi 241	. . . . . . 7 ⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ¬ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
128	1, 127	syl5bir 242	. . . . . 6 ⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (¬ ¬ ∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ¬ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
129	128	orrd 860	. . . . 5 ⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (¬ ∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∨ ¬ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
130		ianor 979	. . . . 5 ⊢ (¬ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∧ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)) ↔ (¬ ∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∨ ¬ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
131	129, 130	sylibr 233	. . . 4 ⊢ (([𝑎⇄𝑏]𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ¬ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∧ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
132	131	ralrimivva 3123	. . 3 ⊢ ([𝑎⇄𝑏]𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ¬ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∧ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
133		ralnex2 3189	. . 3 ⊢ (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ¬ (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∧ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)) ↔ ¬ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∧ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
134	132, 133	sylib 217	. 2 ⊢ ([𝑎⇄𝑏]𝜑 → ¬ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∧ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
135		eqeq1 2742	. . . . 5 ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (𝑝 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))
136	135	3anbi1d 1439	. . . 4 ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → ((𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)))
137	136	2exbidv 1927	. . 3 ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (∃𝑎∃𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ ∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)))
138		eqeq1 2742	. . . . 5 ⊢ (𝑝 = ⟨𝑣, 𝑤⟩ → (𝑝 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩))
139	138	3anbi1d 1439	. . . 4 ⊢ (𝑝 = ⟨𝑣, 𝑤⟩ → ((𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ (⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)))
140	139	2exbidv 1927	. . 3 ⊢ (𝑝 = ⟨𝑣, 𝑤⟩ → (∃𝑎∃𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ ∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑)))
141	137, 140	reuop 6196	. 2 ⊢ (∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎∃𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) ∧ ∀𝑣 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∃𝑎∃𝑏(⟨𝑣, 𝑤⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑) → ⟨𝑣, 𝑤⟩ = ⟨𝑥, 𝑦⟩)))
142	134, 141	sylnibr 329	1 ⊢ ([𝑎⇄𝑏]𝜑 → ¬ ∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎∃𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 844   ∧ w3a 1086  ∀wal 1537   = wceq 1539  ∃wex 1782  [wsb 2067   ∈ wcel 2106   ≠ wne 2943  ∀wral 3064  ∃wrex 3065  ∃!wreu 3066  [wsbc 3716  ⟨cop 4567   × cxp 5587  [wich 44897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-opab 5137  df-xp 5595  df-ich 44898

This theorem is referenced by: (None)