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

Theorem icheq 44348
 Description: In an equality of setvar variables, the setvar variables are interchangeable. (Contributed by AV, 29-Jul-2023.)
Assertion
Ref Expression
icheq [𝑥𝑦]𝑥 = 𝑦
Distinct variable group:   𝑥,𝑦

Proof of Theorem icheq
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 equsb3r 2108 . . . . 5 ([𝑧 / 𝑦]𝑥 = 𝑦𝑥 = 𝑧)
212sbbii 2083 . . . 4 ([𝑥 / 𝑧][𝑦 / 𝑥][𝑧 / 𝑦]𝑥 = 𝑦 ↔ [𝑥 / 𝑧][𝑦 / 𝑥]𝑥 = 𝑧)
3 equsb3 2107 . . . . 5 ([𝑦 / 𝑥]𝑥 = 𝑧𝑦 = 𝑧)
43sbbii 2082 . . . 4 ([𝑥 / 𝑧][𝑦 / 𝑥]𝑥 = 𝑧 ↔ [𝑥 / 𝑧]𝑦 = 𝑧)
5 equsb3r 2108 . . . . 5 ([𝑥 / 𝑧]𝑦 = 𝑧𝑦 = 𝑥)
6 equcom 2026 . . . . 5 (𝑦 = 𝑥𝑥 = 𝑦)
75, 6bitri 278 . . . 4 ([𝑥 / 𝑧]𝑦 = 𝑧𝑥 = 𝑦)
82, 4, 73bitri 301 . . 3 ([𝑥 / 𝑧][𝑦 / 𝑥][𝑧 / 𝑦]𝑥 = 𝑦𝑥 = 𝑦)
98gen2 1799 . 2 𝑥𝑦([𝑥 / 𝑧][𝑦 / 𝑥][𝑧 / 𝑦]𝑥 = 𝑦𝑥 = 𝑦)
10 df-ich 44332 . 2 ([𝑥𝑦]𝑥 = 𝑦 ↔ ∀𝑥𝑦([𝑥 / 𝑧][𝑦 / 𝑥][𝑧 / 𝑦]𝑥 = 𝑦𝑥 = 𝑦))
119, 10mpbir 234 1 [𝑥𝑦]𝑥 = 𝑦
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209  ∀wal 1537  [wsb 2070  [wich 44331 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016 This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1783  df-sb 2071  df-ich 44332 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator