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 [ 𝑎 ⇄ 𝑏 ] ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 )

Proof

Step Hyp Ref Expression
1 equequ1 ⊢ ( 𝑎 = 𝑡 → ( 𝑎 = 𝑏 ↔ 𝑡 = 𝑏 ) )
2 neeq1 ⊢ ( 𝑎 = 𝑡 → ( 𝑎 ≠ 𝑐 ↔ 𝑡 ≠ 𝑐 ) )
3 1 2 3anbi12d ⊢ ( 𝑎 = 𝑡 → ( ( 𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ↔ ( 𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ) )
4 3 2exbidv ⊢ ( 𝑎 = 𝑡 → ( ∃ 𝑏 ∃ 𝑐 ( 𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ↔ ∃ 𝑏 ∃ 𝑐 ( 𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ) )
5 4 cbvexvw ⊢ ( ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ↔ ∃ 𝑡 ∃ 𝑏 ∃ 𝑐 ( 𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) )
6 5 a1i ⊢ ( 𝑎 = 𝑡 → ( ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ↔ ∃ 𝑡 ∃ 𝑏 ∃ 𝑐 ( 𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ) )
7 equequ2 ⊢ ( 𝑏 = 𝑎 → ( 𝑡 = 𝑏 ↔ 𝑡 = 𝑎 ) )
8 neeq1 ⊢ ( 𝑏 = 𝑎 → ( 𝑏 ≠ 𝑐 ↔ 𝑎 ≠ 𝑐 ) )
9 7 8 3anbi13d ⊢ ( 𝑏 = 𝑎 → ( ( 𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ↔ ( 𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐 ) ) )
10 9 exbidv ⊢ ( 𝑏 = 𝑎 → ( ∃ 𝑐 ( 𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ↔ ∃ 𝑐 ( 𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐 ) ) )
11 10 cbvexvw ⊢ ( ∃ 𝑏 ∃ 𝑐 ( 𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ↔ ∃ 𝑎 ∃ 𝑐 ( 𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐 ) )
12 11 exbii ⊢ ( ∃ 𝑡 ∃ 𝑏 ∃ 𝑐 ( 𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ↔ ∃ 𝑡 ∃ 𝑎 ∃ 𝑐 ( 𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐 ) )
13 12 a1i ⊢ ( 𝑏 = 𝑎 → ( ∃ 𝑡 ∃ 𝑏 ∃ 𝑐 ( 𝑡 = 𝑏 ∧ 𝑡 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ↔ ∃ 𝑡 ∃ 𝑎 ∃ 𝑐 ( 𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐 ) ) )
14 equequ1 ⊢ ( 𝑡 = 𝑏 → ( 𝑡 = 𝑎 ↔ 𝑏 = 𝑎 ) )
15 neeq1 ⊢ ( 𝑡 = 𝑏 → ( 𝑡 ≠ 𝑐 ↔ 𝑏 ≠ 𝑐 ) )
16 14 15 3anbi12d ⊢ ( 𝑡 = 𝑏 → ( ( 𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐 ) ↔ ( 𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐 ) ) )
17 16 2exbidv ⊢ ( 𝑡 = 𝑏 → ( ∃ 𝑎 ∃ 𝑐 ( 𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐 ) ↔ ∃ 𝑎 ∃ 𝑐 ( 𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐 ) ) )
18 17 cbvexvw ⊢ ( ∃ 𝑡 ∃ 𝑎 ∃ 𝑐 ( 𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐 ) ↔ ∃ 𝑏 ∃ 𝑎 ∃ 𝑐 ( 𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐 ) )
19 excom ⊢ ( ∃ 𝑏 ∃ 𝑎 ∃ 𝑐 ( 𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐 ) ↔ ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐 ) )
20 3ancomb ⊢ ( ( 𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐 ) ↔ ( 𝑏 = 𝑎 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) )
21 equcom ⊢ ( 𝑏 = 𝑎 ↔ 𝑎 = 𝑏 )
22 21 3anbi1i ⊢ ( ( 𝑏 = 𝑎 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ↔ ( 𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) )
23 20 22 bitri ⊢ ( ( 𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐 ) ↔ ( 𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) )
24 23 3exbii ⊢ ( ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐 ) ↔ ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) )
25 19 24 bitri ⊢ ( ∃ 𝑏 ∃ 𝑎 ∃ 𝑐 ( 𝑏 = 𝑎 ∧ 𝑏 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐 ) ↔ ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) )
26 18 25 bitri ⊢ ( ∃ 𝑡 ∃ 𝑎 ∃ 𝑐 ( 𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐 ) ↔ ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) )
27 26 a1i ⊢ ( 𝑡 = 𝑏 → ( ∃ 𝑡 ∃ 𝑎 ∃ 𝑐 ( 𝑡 = 𝑎 ∧ 𝑡 ≠ 𝑐 ∧ 𝑎 ≠ 𝑐 ) ↔ ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 ) ) )
28 6 13 27 ichcircshi ⊢ [ 𝑎 ⇄ 𝑏 ] ∃ 𝑎 ∃ 𝑏 ∃ 𝑐 ( 𝑎 = 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑏 ≠ 𝑐 )