MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sbcom2 Structured version   Visualization version   GIF version

Theorem sbcom2 2158
Description: Commutativity law for substitution. Used in proof of Theorem 9.7 of [Megill] p. 449 (p. 16 of the preprint). (Contributed by NM, 27-May-1997.) (Proof shortened by Wolf Lammen, 23-Dec-2022.)
Assertion
Ref Expression
sbcom2 ([𝑤 / 𝑧][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑)
Distinct variable groups:   𝑥,𝑧   𝑥,𝑤   𝑦,𝑧
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑤)

Proof of Theorem sbcom2
Dummy variables 𝑣 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 2sb6 2085 . . . . . . . . 9 ([𝑣 / 𝑧][𝑢 / 𝑥]𝜑 ↔ ∀𝑧𝑥((𝑧 = 𝑣𝑥 = 𝑢) → 𝜑))
2 alcom 2153 . . . . . . . . 9 (∀𝑧𝑥((𝑧 = 𝑣𝑥 = 𝑢) → 𝜑) ↔ ∀𝑥𝑧((𝑧 = 𝑣𝑥 = 𝑢) → 𝜑))
3 ancomst 465 . . . . . . . . . 10 (((𝑧 = 𝑣𝑥 = 𝑢) → 𝜑) ↔ ((𝑥 = 𝑢𝑧 = 𝑣) → 𝜑))
432albii 1812 . . . . . . . . 9 (∀𝑥𝑧((𝑧 = 𝑣𝑥 = 𝑢) → 𝜑) ↔ ∀𝑥𝑧((𝑥 = 𝑢𝑧 = 𝑣) → 𝜑))
51, 2, 43bitri 298 . . . . . . . 8 ([𝑣 / 𝑧][𝑢 / 𝑥]𝜑 ↔ ∀𝑥𝑧((𝑥 = 𝑢𝑧 = 𝑣) → 𝜑))
6 2sb6 2085 . . . . . . . 8 ([𝑢 / 𝑥][𝑣 / 𝑧]𝜑 ↔ ∀𝑥𝑧((𝑥 = 𝑢𝑧 = 𝑣) → 𝜑))
75, 6bitr4i 279 . . . . . . 7 ([𝑣 / 𝑧][𝑢 / 𝑥]𝜑 ↔ [𝑢 / 𝑥][𝑣 / 𝑧]𝜑)
8 sbequ 2081 . . . . . . . 8 (𝑢 = 𝑦 → ([𝑢 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
98sbbidv 2075 . . . . . . 7 (𝑢 = 𝑦 → ([𝑣 / 𝑧][𝑢 / 𝑥]𝜑 ↔ [𝑣 / 𝑧][𝑦 / 𝑥]𝜑))
107, 9syl5bbr 286 . . . . . 6 (𝑢 = 𝑦 → ([𝑢 / 𝑥][𝑣 / 𝑧]𝜑 ↔ [𝑣 / 𝑧][𝑦 / 𝑥]𝜑))
11 sbequ 2081 . . . . . 6 (𝑣 = 𝑤 → ([𝑣 / 𝑧][𝑦 / 𝑥]𝜑 ↔ [𝑤 / 𝑧][𝑦 / 𝑥]𝜑))
1210, 11sylan9bb 510 . . . . 5 ((𝑢 = 𝑦𝑣 = 𝑤) → ([𝑢 / 𝑥][𝑣 / 𝑧]𝜑 ↔ [𝑤 / 𝑧][𝑦 / 𝑥]𝜑))
13 sbequ 2081 . . . . . . 7 (𝑣 = 𝑤 → ([𝑣 / 𝑧]𝜑 ↔ [𝑤 / 𝑧]𝜑))
1413sbbidv 2075 . . . . . 6 (𝑣 = 𝑤 → ([𝑢 / 𝑥][𝑣 / 𝑧]𝜑 ↔ [𝑢 / 𝑥][𝑤 / 𝑧]𝜑))
15 sbequ 2081 . . . . . 6 (𝑢 = 𝑦 → ([𝑢 / 𝑥][𝑤 / 𝑧]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑))
1614, 15sylan9bbr 511 . . . . 5 ((𝑢 = 𝑦𝑣 = 𝑤) → ([𝑢 / 𝑥][𝑣 / 𝑧]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑))
1712, 16bitr3d 282 . . . 4 ((𝑢 = 𝑦𝑣 = 𝑤) → ([𝑤 / 𝑧][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑))
1817ex 413 . . 3 (𝑢 = 𝑦 → (𝑣 = 𝑤 → ([𝑤 / 𝑧][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑)))
19 ax6ev 1963 . . 3 𝑢 𝑢 = 𝑦
2018, 19exlimiiv 1923 . 2 (𝑣 = 𝑤 → ([𝑤 / 𝑧][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑))
21 ax6ev 1963 . 2 𝑣 𝑣 = 𝑤
2220, 21exlimiiv 1923 1 ([𝑤 / 𝑧][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wal 1526  [wsb 2060
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-11 2151
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-sb 2061
This theorem is referenced by:  sbco4lem  2275  sbco4  2276  2mo  2729  cnvopab  5991  2reu8i  43193  dfich2bi  43462  ichcom  43464  ichbi12i  43465
  Copyright terms: Public domain W3C validator