Theorem ichexmpl1 48036

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 2044	. . . . . 6 ⊢ (𝑎 = 𝑡 → (𝑎 = 𝑏 ↔ 𝑡 = 𝑏))
2		neeq1 3018	. . . . . 6 ⊢ (𝑎 = 𝑡 → (𝑎 ≠ 𝑐 ↔ 𝑡 ≠ 𝑐))
3	1, 2	3anbi12d 1457	. . . . 5 ⊢ (𝑎 = 𝑡 → ((𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ (𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)))
4	3	2exbidv 1943	. . . 4 ⊢ (𝑎 = 𝑡 → (∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑏∃𝑐(𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)))
5	4	cbvexvw 2056	. . 3 ⊢ (∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑡∃𝑏∃𝑐(𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))
6	5	a1i 11	. 2 ⊢ (𝑎 = 𝑡 → (∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑡∃𝑏∃𝑐(𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)))
7		equequ2 2045	. . . . . . 7 ⊢ (𝑏 = 𝑎 → (𝑡 = 𝑏 ↔ 𝑡 = 𝑎))
8		neeq1 3018	. . . . . . 7 ⊢ (𝑏 = 𝑎 → (𝑏 ≠ 𝑐 ↔ 𝑎 ≠ 𝑐))
9	7, 8	3anbi13d 1458	. . . . . 6 ⊢ (𝑏 = 𝑎 → ((𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ (𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐)))
10	9	exbidv 1940	. . . . 5 ⊢ (𝑏 = 𝑎 → (∃𝑐(𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐)))
11	10	cbvexvw 2056	. . . 4 ⊢ (∃𝑏∃𝑐(𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑎∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐))
12	11	exbii 1867	. . 3 ⊢ (∃𝑡∃𝑏∃𝑐(𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑡∃𝑎∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐))
13	12	a1i 11	. 2 ⊢ (𝑏 = 𝑎 → (∃𝑡∃𝑏∃𝑐(𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑡∃𝑎∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐)))
14		equequ1 2044	. . . . . . 7 ⊢ (𝑡 = 𝑏 → (𝑡 = 𝑎 ↔ 𝑏 = 𝑎))
15		neeq1 3018	. . . . . . 7 ⊢ (𝑡 = 𝑏 → (𝑡 ≠ 𝑐 ↔ 𝑏 ≠ 𝑐))
16	14, 15	3anbi12d 1457	. . . . . 6 ⊢ (𝑡 = 𝑏 → ((𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ (𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐)))
17	16	2exbidv 1943	. . . . 5 ⊢ (𝑡 = 𝑏 → (∃𝑎∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ ∃𝑎∃𝑐(𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐)))
18	17	cbvexvw 2056	. . . 4 ⊢ (∃𝑡∃𝑎∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ ∃𝑏∃𝑎∃𝑐(𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐))
19		excom 2195	. . . . 5 ⊢ (∃𝑏∃𝑎∃𝑐(𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ ∃𝑎∃𝑏∃𝑐(𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐))
20		3ancomb 1110	. . . . . . 7 ⊢ ((𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ (𝑏 = 𝑎 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))
21		equcom 2037	. . . . . . . 8 ⊢ (𝑏 = 𝑎 ↔ 𝑎 = 𝑏)
22	21	3anbi1i 1169	. . . . . . 7 ⊢ ((𝑏 = 𝑎 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ (𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))
23	20, 22	bitri 277	. . . . . 6 ⊢ ((𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ (𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))
24	23	3exbii 1869	. . . . 5 ⊢ (∃𝑎∃𝑏∃𝑐(𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ ∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))
25	19, 24	bitri 277	. . . 4 ⊢ (∃𝑏∃𝑎∃𝑐(𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ ∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))
26	18, 25	bitri 277	. . 3 ⊢ (∃𝑡∃𝑎∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ ∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))
27	26	a1i 11	. 2 ⊢ (𝑡 = 𝑏 → (∃𝑡∃𝑎∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ ∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)))
28	6, 13, 27	ichcircshi 48021	1 ⊢ [𝑎⇄𝑏]∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)

Syntax hints:   ↔ wb 208   ∧ w3a 1097  ∃wex 1798   ≠ wne 2956  [wich 48012

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-11 2190  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1099  df-ex 1799  df-sb 2090  df-cleq 2753  df-ne 2957  df-ich 48013

This theorem is referenced by: (None)