Metamath Proof Explorer

Theorem 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∃a∃b∃ca=b∧a≠c∧b≠c

Proof

Step Hyp Ref Expression
1 equequ1 ⊢a=t→a=b↔t=b
2 neeq1 ⊢a=t→a≠c↔t≠c
3 1 2 3anbi12d ⊢a=t→a=b∧a≠c∧b≠c↔t=b∧t≠c∧b≠c
4 3 2exbidv ⊢a=t→∃b∃ca=b∧a≠c∧b≠c↔∃b∃ct=b∧t≠c∧b≠c
5 4 cbvexvw ⊢∃a∃b∃ca=b∧a≠c∧b≠c↔∃t∃b∃ct=b∧t≠c∧b≠c
6 5 a1i ⊢a=t→∃a∃b∃ca=b∧a≠c∧b≠c↔∃t∃b∃ct=b∧t≠c∧b≠c
7 equequ2 ⊢b=a→t=b↔t=a
8 neeq1 ⊢b=a→b≠c↔a≠c
9 7 8 3anbi13d ⊢b=a→t=b∧t≠c∧b≠c↔t=a∧t≠c∧a≠c
10 9 exbidv ⊢b=a→∃ct=b∧t≠c∧b≠c↔∃ct=a∧t≠c∧a≠c
11 10 cbvexvw ⊢∃b∃ct=b∧t≠c∧b≠c↔∃a∃ct=a∧t≠c∧a≠c
12 11 exbii ⊢∃t∃b∃ct=b∧t≠c∧b≠c↔∃t∃a∃ct=a∧t≠c∧a≠c
13 12 a1i ⊢b=a→∃t∃b∃ct=b∧t≠c∧b≠c↔∃t∃a∃ct=a∧t≠c∧a≠c
14 equequ1 ⊢t=b→t=a↔b=a
15 neeq1 ⊢t=b→t≠c↔b≠c
16 14 15 3anbi12d ⊢t=b→t=a∧t≠c∧a≠c↔b=a∧b≠c∧a≠c
17 16 2exbidv ⊢t=b→∃a∃ct=a∧t≠c∧a≠c↔∃a∃cb=a∧b≠c∧a≠c
18 17 cbvexvw ⊢∃t∃a∃ct=a∧t≠c∧a≠c↔∃b∃a∃cb=a∧b≠c∧a≠c
19 excom ⊢∃b∃a∃cb=a∧b≠c∧a≠c↔∃a∃b∃cb=a∧b≠c∧a≠c
20 3ancomb ⊢b=a∧b≠c∧a≠c↔b=a∧a≠c∧b≠c
21 equcom ⊢b=a↔a=b
22 21 3anbi1i ⊢b=a∧a≠c∧b≠c↔a=b∧a≠c∧b≠c
23 20 22 bitri ⊢b=a∧b≠c∧a≠c↔a=b∧a≠c∧b≠c
24 23 3exbii ⊢∃a∃b∃cb=a∧b≠c∧a≠c↔∃a∃b∃ca=b∧a≠c∧b≠c
25 19 24 bitri ⊢∃b∃a∃cb=a∧b≠c∧a≠c↔∃a∃b∃ca=b∧a≠c∧b≠c
26 18 25 bitri ⊢∃t∃a∃ct=a∧t≠c∧a≠c↔∃a∃b∃ca=b∧a≠c∧b≠c
27 26 a1i ⊢t=b→∃t∃a∃ct=a∧t≠c∧a≠c↔∃a∃b∃ca=b∧a≠c∧b≠c
28 6 13 27 ichcircshi ⊢a⇄b∃a∃b∃ca=b∧a≠c∧b≠c