ichexmpl1

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

		Ref	Expression
	Assertion	ichexmpl1	$⊢ [a ⇄ b] \exists a \exists b \exists c (a = b \land a \neq c \land b \neq c)$

Proof

Step	Hyp	Ref	Expression
1		equequ1	$⊢ a = t \to (a = b \leftrightarrow t = b)$
2		neeq1	$⊢ a = t \to (a \neq c \leftrightarrow t \neq c)$
3	1 2	3anbi12d	$⊢ a = t \to ((a = b \land a \neq c \land b \neq c) \leftrightarrow (t = b \land t \neq c \land b \neq c))$
4	3	2exbidv	$⊢ a = t \to (\exists b \exists c (a = b \land a \neq c \land b \neq c) \leftrightarrow \exists b \exists c (t = b \land t \neq c \land b \neq c))$
5	4	cbvexvw	$⊢ \exists a \exists b \exists c (a = b \land a \neq c \land b \neq c) \leftrightarrow \exists t \exists b \exists c (t = b \land t \neq c \land b \neq c)$
6	5	a1i	$⊢ a = t \to (\exists a \exists b \exists c (a = b \land a \neq c \land b \neq c) \leftrightarrow \exists t \exists b \exists c (t = b \land t \neq c \land b \neq c))$
7		equequ2	$⊢ b = a \to (t = b \leftrightarrow t = a)$
8		neeq1	$⊢ b = a \to (b \neq c \leftrightarrow a \neq c)$
9	7 8	3anbi13d	$⊢ b = a \to ((t = b \land t \neq c \land b \neq c) \leftrightarrow (t = a \land t \neq c \land a \neq c))$
10	9	exbidv	$⊢ b = a \to (\exists c (t = b \land t \neq c \land b \neq c) \leftrightarrow \exists c (t = a \land t \neq c \land a \neq c))$
11	10	cbvexvw	$⊢ \exists b \exists c (t = b \land t \neq c \land b \neq c) \leftrightarrow \exists a \exists c (t = a \land t \neq c \land a \neq c)$
12	11	exbii	$⊢ \exists t \exists b \exists c (t = b \land t \neq c \land b \neq c) \leftrightarrow \exists t \exists a \exists c (t = a \land t \neq c \land a \neq c)$
13	12	a1i	$⊢ b = a \to (\exists t \exists b \exists c (t = b \land t \neq c \land b \neq c) \leftrightarrow \exists t \exists a \exists c (t = a \land t \neq c \land a \neq c))$
14		equequ1	$⊢ t = b \to (t = a \leftrightarrow b = a)$
15		neeq1	$⊢ t = b \to (t \neq c \leftrightarrow b \neq c)$
16	14 15	3anbi12d	$⊢ t = b \to ((t = a \land t \neq c \land a \neq c) \leftrightarrow (b = a \land b \neq c \land a \neq c))$
17	16	2exbidv	$⊢ t = b \to (\exists a \exists c (t = a \land t \neq c \land a \neq c) \leftrightarrow \exists a \exists c (b = a \land b \neq c \land a \neq c))$
18	17	cbvexvw	$⊢ \exists t \exists a \exists c (t = a \land t \neq c \land a \neq c) \leftrightarrow \exists b \exists a \exists c (b = a \land b \neq c \land a \neq c)$
19		excom	$⊢ \exists b \exists a \exists c (b = a \land b \neq c \land a \neq c) \leftrightarrow \exists a \exists b \exists c (b = a \land b \neq c \land a \neq c)$
20		3ancomb	$⊢ (b = a \land b \neq c \land a \neq c) \leftrightarrow (b = a \land a \neq c \land b \neq c)$
21		equcom	$⊢ b = a \leftrightarrow a = b$
22	21	3anbi1i	$⊢ (b = a \land a \neq c \land b \neq c) \leftrightarrow (a = b \land a \neq c \land b \neq c)$
23	20 22	bitri	$⊢ (b = a \land b \neq c \land a \neq c) \leftrightarrow (a = b \land a \neq c \land b \neq c)$
24	23	3exbii	$⊢ \exists a \exists b \exists c (b = a \land b \neq c \land a \neq c) \leftrightarrow \exists a \exists b \exists c (a = b \land a \neq c \land b \neq c)$
25	19 24	bitri	$⊢ \exists b \exists a \exists c (b = a \land b \neq c \land a \neq c) \leftrightarrow \exists a \exists b \exists c (a = b \land a \neq c \land b \neq c)$
26	18 25	bitri	$⊢ \exists t \exists a \exists c (t = a \land t \neq c \land a \neq c) \leftrightarrow \exists a \exists b \exists c (a = b \land a \neq c \land b \neq c)$
27	26	a1i	$⊢ t = b \to (\exists t \exists a \exists c (t = a \land t \neq c \land a \neq c) \leftrightarrow \exists a \exists b \exists c (a = b \land a \neq c \land b \neq c))$
28	6 13 27	ichcircshi	$⊢ [a ⇄ b] \exists a \exists b \exists c (a = b \land a \neq c \land b \neq c)$

Metamath Proof Explorer

Theorem ichexmpl1

Proof