Theorem ichexmpl1 47394

Description: Example for interchangeable setvar variables in a statement of predicate calculus with equality. (Contributed by AV, 31-Jul-2023.)

Assertion

Ref	Expression
ichexmpl1	⊢ [𝑎⇄𝑏]∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)

Distinct variable group:   𝑎,𝑏,𝑐

Proof of Theorem ichexmpl1

Dummy variable 𝑡 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		equequ1 2022	. . . . . 6 ⊢ (𝑎 = 𝑡 → (𝑎 = 𝑏 ↔ 𝑡 = 𝑏))
2		neeq1 3001	. . . . . 6 ⊢ (𝑎 = 𝑡 → (𝑎 ≠ 𝑐 ↔ 𝑡 ≠ 𝑐))
3	1, 2	3anbi12d 1436	. . . . 5 ⊢ (𝑎 = 𝑡 → ((𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ (𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)))
4	3	2exbidv 1922	. . . 4 ⊢ (𝑎 = 𝑡 → (∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑏∃𝑐(𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)))
5	4	cbvexvw 2034	. . 3 ⊢ (∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑡∃𝑏∃𝑐(𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))
6	5	a1i 11	. 2 ⊢ (𝑎 = 𝑡 → (∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑡∃𝑏∃𝑐(𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)))
7		equequ2 2023	. . . . . . 7 ⊢ (𝑏 = 𝑎 → (𝑡 = 𝑏 ↔ 𝑡 = 𝑎))
8		neeq1 3001	. . . . . . 7 ⊢ (𝑏 = 𝑎 → (𝑏 ≠ 𝑐 ↔ 𝑎 ≠ 𝑐))
9	7, 8	3anbi13d 1437	. . . . . 6 ⊢ (𝑏 = 𝑎 → ((𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ (𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐)))
10	9	exbidv 1919	. . . . 5 ⊢ (𝑏 = 𝑎 → (∃𝑐(𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐)))
11	10	cbvexvw 2034	. . . 4 ⊢ (∃𝑏∃𝑐(𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑎∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐))
12	11	exbii 1845	. . 3 ⊢ (∃𝑡∃𝑏∃𝑐(𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑡∃𝑎∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐))
13	12	a1i 11	. 2 ⊢ (𝑏 = 𝑎 → (∃𝑡∃𝑏∃𝑐(𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑡∃𝑎∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐)))
14		equequ1 2022	. . . . . . 7 ⊢ (𝑡 = 𝑏 → (𝑡 = 𝑎 ↔ 𝑏 = 𝑎))
15		neeq1 3001	. . . . . . 7 ⊢ (𝑡 = 𝑏 → (𝑡 ≠ 𝑐 ↔ 𝑏 ≠ 𝑐))
16	14, 15	3anbi12d 1436	. . . . . 6 ⊢ (𝑡 = 𝑏 → ((𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ (𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐)))
17	16	2exbidv 1922	. . . . 5 ⊢ (𝑡 = 𝑏 → (∃𝑎∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ ∃𝑎∃𝑐(𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐)))
18	17	cbvexvw 2034	. . . 4 ⊢ (∃𝑡∃𝑎∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ ∃𝑏∃𝑎∃𝑐(𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐))
19		excom 2160	. . . . 5 ⊢ (∃𝑏∃𝑎∃𝑐(𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ ∃𝑎∃𝑏∃𝑐(𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐))
20		3ancomb 1098	. . . . . . 7 ⊢ ((𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ (𝑏 = 𝑎 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))
21		equcom 2015	. . . . . . . 8 ⊢ (𝑏 = 𝑎 ↔ 𝑎 = 𝑏)
22	21	3anbi1i 1156	. . . . . . 7 ⊢ ((𝑏 = 𝑎 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ (𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))
23	20, 22	bitri 275	. . . . . 6 ⊢ ((𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ (𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))
24	23	3exbii 1847	. . . . 5 ⊢ (∃𝑎∃𝑏∃𝑐(𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ ∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))
25	19, 24	bitri 275	. . . 4 ⊢ (∃𝑏∃𝑎∃𝑐(𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ ∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))
26	18, 25	bitri 275	. . 3 ⊢ (∃𝑡∃𝑎∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ ∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))
27	26	a1i 11	. 2 ⊢ (𝑡 = 𝑏 → (∃𝑡∃𝑎∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ ∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)))
28	6, 13, 27	ichcircshi 47379	1 ⊢ [𝑎⇄𝑏]∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)

Syntax hints:   ↔ wb 206   ∧ w3a 1086  ∃wex 1776   ≠ wne 2938  [wich 47370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-11 2155  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1777  df-sb 2063  df-cleq 2727  df-ne 2939  df-ich 47371

This theorem is referenced by: (None)