Theorem ichexmpl1 43680

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 2032	. . . . . 6 ⊢ (𝑎 = 𝑡 → (𝑎 = 𝑏 ↔ 𝑡 = 𝑏))
2		neeq1 3078	. . . . . 6 ⊢ (𝑎 = 𝑡 → (𝑎 ≠ 𝑐 ↔ 𝑡 ≠ 𝑐))
3	1, 2	3anbi12d 1433	. . . . 5 ⊢ (𝑎 = 𝑡 → ((𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ (𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)))
4	3	2exbidv 1925	. . . 4 ⊢ (𝑎 = 𝑡 → (∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑏∃𝑐(𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)))
5	4	cbvexvw 2044	. . 3 ⊢ (∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑡∃𝑏∃𝑐(𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))
6	5	a1i 11	. 2 ⊢ (𝑎 = 𝑡 → (∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑡∃𝑏∃𝑐(𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)))
7		equequ2 2033	. . . . . . 7 ⊢ (𝑏 = 𝑎 → (𝑡 = 𝑏 ↔ 𝑡 = 𝑎))
8		neeq1 3078	. . . . . . 7 ⊢ (𝑏 = 𝑎 → (𝑏 ≠ 𝑐 ↔ 𝑎 ≠ 𝑐))
9	7, 8	3anbi13d 1434	. . . . . 6 ⊢ (𝑏 = 𝑎 → ((𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ (𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐)))
10	9	exbidv 1922	. . . . 5 ⊢ (𝑏 = 𝑎 → (∃𝑐(𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐)))
11	10	cbvexvw 2044	. . . 4 ⊢ (∃𝑏∃𝑐(𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑎∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐))
12	11	exbii 1848	. . 3 ⊢ (∃𝑡∃𝑏∃𝑐(𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑡∃𝑎∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐))
13	12	a1i 11	. 2 ⊢ (𝑏 = 𝑎 → (∃𝑡∃𝑏∃𝑐(𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ ∃𝑡∃𝑎∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐)))
14		equequ1 2032	. . . . . . 7 ⊢ (𝑡 = 𝑏 → (𝑡 = 𝑎 ↔ 𝑏 = 𝑎))
15		neeq1 3078	. . . . . . 7 ⊢ (𝑡 = 𝑏 → (𝑡 ≠ 𝑐 ↔ 𝑏 ≠ 𝑐))
16	14, 15	3anbi12d 1433	. . . . . 6 ⊢ (𝑡 = 𝑏 → ((𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ (𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐)))
17	16	2exbidv 1925	. . . . 5 ⊢ (𝑡 = 𝑏 → (∃𝑎∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ ∃𝑎∃𝑐(𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐)))
18	17	cbvexvw 2044	. . . 4 ⊢ (∃𝑡∃𝑎∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ ∃𝑏∃𝑎∃𝑐(𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐))
19		excom 2169	. . . . 5 ⊢ (∃𝑏∃𝑎∃𝑐(𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ ∃𝑎∃𝑏∃𝑐(𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐))
20		3ancomb 1095	. . . . . . 7 ⊢ ((𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ (𝑏 = 𝑎 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))
21		equcom 2025	. . . . . . . 8 ⊢ (𝑏 = 𝑎 ↔ 𝑎 = 𝑏)
22	21	3anbi1i 1153	. . . . . . 7 ⊢ ((𝑏 = 𝑎 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐) ↔ (𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))
23	20, 22	bitri 277	. . . . . 6 ⊢ ((𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ (𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))
24	23	3exbii 1850	. . . . 5 ⊢ (∃𝑎∃𝑏∃𝑐(𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ ∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))
25	19, 24	bitri 277	. . . 4 ⊢ (∃𝑏∃𝑎∃𝑐(𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ ∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))
26	18, 25	bitri 277	. . 3 ⊢ (∃𝑡∃𝑎∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ ∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐))
27	26	a1i 11	. 2 ⊢ (𝑡 = 𝑏 → (∃𝑡∃𝑎∃𝑐(𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐) ↔ ∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)))
28	6, 13, 27	ichcircshi 43661	1 ⊢ [𝑎⇄𝑏]∃𝑎∃𝑏∃𝑐(𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐)

Syntax hints:   ↔ wb 208   ∧ w3a 1083  ∃wex 1780   ≠ wne 3016  [wich 43654

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-11 2161  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-3an 1085  df-ex 1781  df-sb 2070  df-cleq 2814  df-ne 3017  df-ich 43655

This theorem is referenced by: (None)