Theorem ichexmpl1 48251

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 2058	. . . . . 6 ⊢ (𝑎 = 𝑡 → (𝑎 = 𝑏 ↔ 𝑡 = 𝑏))
2		neeq1 3022	. . . . . 6 ⊢ (𝑎 = 𝑡 → (𝑎 ≠ 𝑐 ↔ 𝑡 ≠ 𝑐))
3	1, 2	3anbi12d 1465	. . . . 5 ⊢ (𝑎 = 𝑡 → ((𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ (𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)))
4	3	2exbidv 1957	. . . 4 ⊢ (𝑎 = 𝑡 → (∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑏∃𝑐(𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)))
5	4	cbvexvw 2070	. . 3 ⊢ (∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑡∃𝑏∃𝑐(𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))
6	5	a1i 11	. 2 ⊢ (𝑎 = 𝑡 → (∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑡∃𝑏∃𝑐(𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)))
7		equequ2 2059	. . . . . . 7 ⊢ (𝑏 = 𝑎 → (𝑡 = 𝑏 ↔ 𝑡 = 𝑎))
8		neeq1 3022	. . . . . . 7 ⊢ (𝑏 = 𝑎 → (𝑏 ≠ 𝑐 ↔ 𝑎 ≠ 𝑐))
9	7, 8	3anbi13d 1466	. . . . . 6 ⊢ (𝑏 = 𝑎 → ((𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ (𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐)))
10	9	exbidv 1954	. . . . 5 ⊢ (𝑏 = 𝑎 → (∃𝑐(𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐)))
11	10	cbvexvw 2070	. . . 4 ⊢ (∃𝑏∃𝑐(𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑎∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐))
12	11	exbii 1881	. . 3 ⊢ (∃𝑡∃𝑏∃𝑐(𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑡∃𝑎∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐))
13	12	a1i 11	. 2 ⊢ (𝑏 = 𝑎 → (∃𝑡∃𝑏∃𝑐(𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑡∃𝑎∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐)))
14		equequ1 2058	. . . . . . 7 ⊢ (𝑡 = 𝑏 → (𝑡 = 𝑎 ↔ 𝑏 = 𝑎))
15		neeq1 3022	. . . . . . 7 ⊢ (𝑡 = 𝑏 → (𝑡 ≠ 𝑐 ↔ 𝑏 ≠ 𝑐))
16	14, 15	3anbi12d 1465	. . . . . 6 ⊢ (𝑡 = 𝑏 → ((𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ (𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐)))
17	16	2exbidv 1957	. . . . 5 ⊢ (𝑡 = 𝑏 → (∃𝑎∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ ∃𝑎∃𝑐(𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐)))
18	17	cbvexvw 2070	. . . 4 ⊢ (∃𝑡∃𝑎∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ ∃𝑏∃𝑎∃𝑐(𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐))
19		excom 2200	. . . . 5 ⊢ (∃𝑏∃𝑎∃𝑐(𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ ∃𝑎∃𝑏∃𝑐(𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐))
20		3ancomb 1116	. . . . . . 7 ⊢ ((𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ (𝑏 = 𝑎 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))
21		equcom 2051	. . . . . . . 8 ⊢ (𝑏 = 𝑎 ↔ 𝑎 = 𝑏)
22	21	3anbi1i 1175	. . . . . . 7 ⊢ ((𝑏 = 𝑎 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ (𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))
23	20, 22	bitri 278	. . . . . 6 ⊢ ((𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ (𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))
24	23	3exbii 1883	. . . . 5 ⊢ (∃𝑎∃𝑏∃𝑐(𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ ∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))
25	19, 24	bitri 278	. . . 4 ⊢ (∃𝑏∃𝑎∃𝑐(𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ ∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))
26	18, 25	bitri 278	. . 3 ⊢ (∃𝑡∃𝑎∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ ∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))
27	26	a1i 11	. 2 ⊢ (𝑡 = 𝑏 → (∃𝑡∃𝑎∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ ∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)))
28	6, 13, 27	ichcircshi 48236	1 ⊢ [𝑎⇄𝑏]∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)

This proof depends on syntax axioms:   ↔ wb 209   ∧ w3a 1103  ∃wex 1812   ≠ wne 2960  [wich 48227

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-11 2195  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1813  df-sb 2100  df-cleq 2757  df-ne 2961  df-ich 48228

This theorem is used by: (None)