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

Theorem sbcom2 2523
 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 2253 . . . . . . . . 9 ([𝑣 / 𝑧][𝑢 / 𝑥]𝜑 ↔ ∀𝑧𝑥((𝑧 = 𝑣𝑥 = 𝑢) → 𝜑))
2 alcom 2152 . . . . . . . . 9 (∀𝑧𝑥((𝑧 = 𝑣𝑥 = 𝑢) → 𝜑) ↔ ∀𝑥𝑧((𝑧 = 𝑣𝑥 = 𝑢) → 𝜑))
3 ancomst 458 . . . . . . . . . 10 (((𝑧 = 𝑣𝑥 = 𝑢) → 𝜑) ↔ ((𝑥 = 𝑢𝑧 = 𝑣) → 𝜑))
432albii 1864 . . . . . . . . 9 (∀𝑥𝑧((𝑧 = 𝑣𝑥 = 𝑢) → 𝜑) ↔ ∀𝑥𝑧((𝑥 = 𝑢𝑧 = 𝑣) → 𝜑))
51, 2, 43bitri 289 . . . . . . . 8 ([𝑣 / 𝑧][𝑢 / 𝑥]𝜑 ↔ ∀𝑥𝑧((𝑥 = 𝑢𝑧 = 𝑣) → 𝜑))
6 2sb6 2253 . . . . . . . 8 ([𝑢 / 𝑥][𝑣 / 𝑧]𝜑 ↔ ∀𝑥𝑧((𝑥 = 𝑢𝑧 = 𝑣) → 𝜑))
75, 6bitr4i 270 . . . . . . 7 ([𝑣 / 𝑧][𝑢 / 𝑥]𝜑 ↔ [𝑢 / 𝑥][𝑣 / 𝑧]𝜑)
8 nfv 1957 . . . . . . . 8 𝑧 𝑢 = 𝑦
9 sbequ 2452 . . . . . . . 8 (𝑢 = 𝑦 → ([𝑢 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
108, 9sbbid 2227 . . . . . . 7 (𝑢 = 𝑦 → ([𝑣 / 𝑧][𝑢 / 𝑥]𝜑 ↔ [𝑣 / 𝑧][𝑦 / 𝑥]𝜑))
117, 10syl5bbr 277 . . . . . 6 (𝑢 = 𝑦 → ([𝑢 / 𝑥][𝑣 / 𝑧]𝜑 ↔ [𝑣 / 𝑧][𝑦 / 𝑥]𝜑))
12 sbequ 2452 . . . . . 6 (𝑣 = 𝑤 → ([𝑣 / 𝑧][𝑦 / 𝑥]𝜑 ↔ [𝑤 / 𝑧][𝑦 / 𝑥]𝜑))
1311, 12sylan9bb 505 . . . . 5 ((𝑢 = 𝑦𝑣 = 𝑤) → ([𝑢 / 𝑥][𝑣 / 𝑧]𝜑 ↔ [𝑤 / 𝑧][𝑦 / 𝑥]𝜑))
14 nfv 1957 . . . . . . 7 𝑥 𝑣 = 𝑤
15 sbequ 2452 . . . . . . 7 (𝑣 = 𝑤 → ([𝑣 / 𝑧]𝜑 ↔ [𝑤 / 𝑧]𝜑))
1614, 15sbbid 2227 . . . . . 6 (𝑣 = 𝑤 → ([𝑢 / 𝑥][𝑣 / 𝑧]𝜑 ↔ [𝑢 / 𝑥][𝑤 / 𝑧]𝜑))
17 sbequ 2452 . . . . . 6 (𝑢 = 𝑦 → ([𝑢 / 𝑥][𝑤 / 𝑧]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑))
1816, 17sylan9bbr 506 . . . . 5 ((𝑢 = 𝑦𝑣 = 𝑤) → ([𝑢 / 𝑥][𝑣 / 𝑧]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑))
1913, 18bitr3d 273 . . . 4 ((𝑢 = 𝑦𝑣 = 𝑤) → ([𝑤 / 𝑧][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑))
2019ex 403 . . 3 (𝑢 = 𝑦 → (𝑣 = 𝑤 → ([𝑤 / 𝑧][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑)))
21 ax6ev 2023 . . 3 𝑢 𝑢 = 𝑦
2220, 21exlimiiv 1974 . 2 (𝑣 = 𝑤 → ([𝑤 / 𝑧][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑))
23 ax6ev 2023 . 2 𝑣 𝑣 = 𝑤
2422, 23exlimiiv 1974 1 ([𝑤 / 𝑧][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386  ∀wal 1599  [wsb 2011 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-ex 1824  df-nf 1828  df-sb 2012 This theorem is referenced by:  sbco4lem  2545  sbco4  2546  2mo  2678  cnvopab  5788  2reu8i  42154
 Copyright terms: Public domain W3C validator