Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ichexmpl1 Structured version   Visualization version   GIF version

Theorem ichexmpl1 44029
 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.
StepHypRef Expression
1 equequ1 2032 . . . . . 6 (𝑎 = 𝑡 → (𝑎 = 𝑏𝑡 = 𝑏))
2 neeq1 3049 . . . . . 6 (𝑎 = 𝑡 → (𝑎𝑐𝑡𝑐))
31, 23anbi12d 1434 . . . . 5 (𝑎 = 𝑡 → ((𝑎 = 𝑏𝑎𝑐𝑏𝑐) ↔ (𝑡 = 𝑏𝑡𝑐𝑏𝑐)))
432exbidv 1925 . . . 4 (𝑎 = 𝑡 → (∃𝑏𝑐(𝑎 = 𝑏𝑎𝑐𝑏𝑐) ↔ ∃𝑏𝑐(𝑡 = 𝑏𝑡𝑐𝑏𝑐)))
54cbvexvw 2044 . . 3 (∃𝑎𝑏𝑐(𝑎 = 𝑏𝑎𝑐𝑏𝑐) ↔ ∃𝑡𝑏𝑐(𝑡 = 𝑏𝑡𝑐𝑏𝑐))
65a1i 11 . 2 (𝑎 = 𝑡 → (∃𝑎𝑏𝑐(𝑎 = 𝑏𝑎𝑐𝑏𝑐) ↔ ∃𝑡𝑏𝑐(𝑡 = 𝑏𝑡𝑐𝑏𝑐)))
7 equequ2 2033 . . . . . . 7 (𝑏 = 𝑎 → (𝑡 = 𝑏𝑡 = 𝑎))
8 neeq1 3049 . . . . . . 7 (𝑏 = 𝑎 → (𝑏𝑐𝑎𝑐))
97, 83anbi13d 1435 . . . . . 6 (𝑏 = 𝑎 → ((𝑡 = 𝑏𝑡𝑐𝑏𝑐) ↔ (𝑡 = 𝑎𝑡𝑐𝑎𝑐)))
109exbidv 1922 . . . . 5 (𝑏 = 𝑎 → (∃𝑐(𝑡 = 𝑏𝑡𝑐𝑏𝑐) ↔ ∃𝑐(𝑡 = 𝑎𝑡𝑐𝑎𝑐)))
1110cbvexvw 2044 . . . 4 (∃𝑏𝑐(𝑡 = 𝑏𝑡𝑐𝑏𝑐) ↔ ∃𝑎𝑐(𝑡 = 𝑎𝑡𝑐𝑎𝑐))
1211exbii 1849 . . 3 (∃𝑡𝑏𝑐(𝑡 = 𝑏𝑡𝑐𝑏𝑐) ↔ ∃𝑡𝑎𝑐(𝑡 = 𝑎𝑡𝑐𝑎𝑐))
1312a1i 11 . 2 (𝑏 = 𝑎 → (∃𝑡𝑏𝑐(𝑡 = 𝑏𝑡𝑐𝑏𝑐) ↔ ∃𝑡𝑎𝑐(𝑡 = 𝑎𝑡𝑐𝑎𝑐)))
14 equequ1 2032 . . . . . . 7 (𝑡 = 𝑏 → (𝑡 = 𝑎𝑏 = 𝑎))
15 neeq1 3049 . . . . . . 7 (𝑡 = 𝑏 → (𝑡𝑐𝑏𝑐))
1614, 153anbi12d 1434 . . . . . 6 (𝑡 = 𝑏 → ((𝑡 = 𝑎𝑡𝑐𝑎𝑐) ↔ (𝑏 = 𝑎𝑏𝑐𝑎𝑐)))
17162exbidv 1925 . . . . 5 (𝑡 = 𝑏 → (∃𝑎𝑐(𝑡 = 𝑎𝑡𝑐𝑎𝑐) ↔ ∃𝑎𝑐(𝑏 = 𝑎𝑏𝑐𝑎𝑐)))
1817cbvexvw 2044 . . . 4 (∃𝑡𝑎𝑐(𝑡 = 𝑎𝑡𝑐𝑎𝑐) ↔ ∃𝑏𝑎𝑐(𝑏 = 𝑎𝑏𝑐𝑎𝑐))
19 excom 2166 . . . . 5 (∃𝑏𝑎𝑐(𝑏 = 𝑎𝑏𝑐𝑎𝑐) ↔ ∃𝑎𝑏𝑐(𝑏 = 𝑎𝑏𝑐𝑎𝑐))
20 3ancomb 1096 . . . . . . 7 ((𝑏 = 𝑎𝑏𝑐𝑎𝑐) ↔ (𝑏 = 𝑎𝑎𝑐𝑏𝑐))
21 equcom 2025 . . . . . . . 8 (𝑏 = 𝑎𝑎 = 𝑏)
22213anbi1i 1154 . . . . . . 7 ((𝑏 = 𝑎𝑎𝑐𝑏𝑐) ↔ (𝑎 = 𝑏𝑎𝑐𝑏𝑐))
2320, 22bitri 278 . . . . . 6 ((𝑏 = 𝑎𝑏𝑐𝑎𝑐) ↔ (𝑎 = 𝑏𝑎𝑐𝑏𝑐))
24233exbii 1851 . . . . 5 (∃𝑎𝑏𝑐(𝑏 = 𝑎𝑏𝑐𝑎𝑐) ↔ ∃𝑎𝑏𝑐(𝑎 = 𝑏𝑎𝑐𝑏𝑐))
2519, 24bitri 278 . . . 4 (∃𝑏𝑎𝑐(𝑏 = 𝑎𝑏𝑐𝑎𝑐) ↔ ∃𝑎𝑏𝑐(𝑎 = 𝑏𝑎𝑐𝑏𝑐))
2618, 25bitri 278 . . 3 (∃𝑡𝑎𝑐(𝑡 = 𝑎𝑡𝑐𝑎𝑐) ↔ ∃𝑎𝑏𝑐(𝑎 = 𝑏𝑎𝑐𝑏𝑐))
2726a1i 11 . 2 (𝑡 = 𝑏 → (∃𝑡𝑎𝑐(𝑡 = 𝑎𝑡𝑐𝑎𝑐) ↔ ∃𝑎𝑏𝑐(𝑎 = 𝑏𝑎𝑐𝑏𝑐)))
286, 13, 27ichcircshi 44014 1 [𝑎𝑏]∃𝑎𝑏𝑐(𝑎 = 𝑏𝑎𝑐𝑏𝑐)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ w3a 1084  ∃wex 1781   ≠ wne 2987  [wich 44005 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-11 2158  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086  df-ex 1782  df-sb 2070  df-cleq 2791  df-ne 2988  df-ich 44006 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator