Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  csbcow GIF version

Theorem csbcow 3042
 Description: Composition law for chained substitutions into a class. Version of csbco 3041 with a disjoint variable condition, which requires fewer axioms. (Contributed by NM, 10-Nov-2005.) (Revised by Gino Giotto, 25-Aug-2024.)
Assertion
Ref Expression
csbcow 𝐴 / 𝑦𝑦 / 𝑥𝐵 = 𝐴 / 𝑥𝐵
Distinct variable groups:   𝑥,𝑦   𝑦,𝐵
Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑥)

Proof of Theorem csbcow
Dummy variables 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-csb 3032 . . . . . 6 𝑦 / 𝑥𝐵 = {𝑧[𝑦 / 𝑥]𝑧𝐵}
21abeq2i 2268 . . . . 5 (𝑧𝑦 / 𝑥𝐵[𝑦 / 𝑥]𝑧𝐵)
32sbcbii 2996 . . . 4 ([𝐴 / 𝑦]𝑧𝑦 / 𝑥𝐵[𝐴 / 𝑦][𝑦 / 𝑥]𝑧𝐵)
4 nfv 1508 . . . . . . . . . 10 𝑦𝑥(𝑥 = 𝑤𝑧𝐵)
5 equequ2 1693 . . . . . . . . . . . 12 (𝑦 = 𝑤 → (𝑥 = 𝑦𝑥 = 𝑤))
65imbi1d 230 . . . . . . . . . . 11 (𝑦 = 𝑤 → ((𝑥 = 𝑦𝑧𝐵) ↔ (𝑥 = 𝑤𝑧𝐵)))
76albidv 1804 . . . . . . . . . 10 (𝑦 = 𝑤 → (∀𝑥(𝑥 = 𝑦𝑧𝐵) ↔ ∀𝑥(𝑥 = 𝑤𝑧𝐵)))
84, 7sbiev 1772 . . . . . . . . 9 ([𝑤 / 𝑦]∀𝑥(𝑥 = 𝑦𝑧𝐵) ↔ ∀𝑥(𝑥 = 𝑤𝑧𝐵))
9 sb6 1866 . . . . . . . . 9 ([𝑤 / 𝑥]𝑧𝐵 ↔ ∀𝑥(𝑥 = 𝑤𝑧𝐵))
108, 9bitr4i 186 . . . . . . . 8 ([𝑤 / 𝑦]∀𝑥(𝑥 = 𝑦𝑧𝐵) ↔ [𝑤 / 𝑥]𝑧𝐵)
11 df-clab 2144 . . . . . . . 8 (𝑤 ∈ {𝑦 ∣ ∀𝑥(𝑥 = 𝑦𝑧𝐵)} ↔ [𝑤 / 𝑦]∀𝑥(𝑥 = 𝑦𝑧𝐵))
12 df-clab 2144 . . . . . . . 8 (𝑤 ∈ {𝑥𝑧𝐵} ↔ [𝑤 / 𝑥]𝑧𝐵)
1310, 11, 123bitr4i 211 . . . . . . 7 (𝑤 ∈ {𝑦 ∣ ∀𝑥(𝑥 = 𝑦𝑧𝐵)} ↔ 𝑤 ∈ {𝑥𝑧𝐵})
1413eqriv 2154 . . . . . 6 {𝑦 ∣ ∀𝑥(𝑥 = 𝑦𝑧𝐵)} = {𝑥𝑧𝐵}
1514eleq2i 2224 . . . . 5 (𝐴 ∈ {𝑦 ∣ ∀𝑥(𝑥 = 𝑦𝑧𝐵)} ↔ 𝐴 ∈ {𝑥𝑧𝐵})
16 df-sbc 2938 . . . . . 6 ([𝐴 / 𝑦][𝑦 / 𝑥]𝑧𝐵𝐴 ∈ {𝑦[𝑦 / 𝑥]𝑧𝐵})
17 df-sbc 2938 . . . . . . . . 9 ([𝑦 / 𝑥]𝑧𝐵𝑦 ∈ {𝑥𝑧𝐵})
18 df-clab 2144 . . . . . . . . . 10 (𝑦 ∈ {𝑥𝑧𝐵} ↔ [𝑦 / 𝑥]𝑧𝐵)
19 sb6 1866 . . . . . . . . . 10 ([𝑦 / 𝑥]𝑧𝐵 ↔ ∀𝑥(𝑥 = 𝑦𝑧𝐵))
2018, 19bitri 183 . . . . . . . . 9 (𝑦 ∈ {𝑥𝑧𝐵} ↔ ∀𝑥(𝑥 = 𝑦𝑧𝐵))
2117, 20bitri 183 . . . . . . . 8 ([𝑦 / 𝑥]𝑧𝐵 ↔ ∀𝑥(𝑥 = 𝑦𝑧𝐵))
2221abbii 2273 . . . . . . 7 {𝑦[𝑦 / 𝑥]𝑧𝐵} = {𝑦 ∣ ∀𝑥(𝑥 = 𝑦𝑧𝐵)}
2322eleq2i 2224 . . . . . 6 (𝐴 ∈ {𝑦[𝑦 / 𝑥]𝑧𝐵} ↔ 𝐴 ∈ {𝑦 ∣ ∀𝑥(𝑥 = 𝑦𝑧𝐵)})
2416, 23bitri 183 . . . . 5 ([𝐴 / 𝑦][𝑦 / 𝑥]𝑧𝐵𝐴 ∈ {𝑦 ∣ ∀𝑥(𝑥 = 𝑦𝑧𝐵)})
25 df-sbc 2938 . . . . 5 ([𝐴 / 𝑥]𝑧𝐵𝐴 ∈ {𝑥𝑧𝐵})
2615, 24, 253bitr4i 211 . . . 4 ([𝐴 / 𝑦][𝑦 / 𝑥]𝑧𝐵[𝐴 / 𝑥]𝑧𝐵)
273, 26bitri 183 . . 3 ([𝐴 / 𝑦]𝑧𝑦 / 𝑥𝐵[𝐴 / 𝑥]𝑧𝐵)
2827abbii 2273 . 2 {𝑧[𝐴 / 𝑦]𝑧𝑦 / 𝑥𝐵} = {𝑧[𝐴 / 𝑥]𝑧𝐵}
29 df-csb 3032 . 2 𝐴 / 𝑦𝑦 / 𝑥𝐵 = {𝑧[𝐴 / 𝑦]𝑧𝑦 / 𝑥𝐵}
30 df-csb 3032 . 2 𝐴 / 𝑥𝐵 = {𝑧[𝐴 / 𝑥]𝑧𝐵}
3128, 29, 303eqtr4i 2188 1 𝐴 / 𝑦𝑦 / 𝑥𝐵 = 𝐴 / 𝑥𝐵
 Colors of variables: wff set class Syntax hints:   → wi 4  ∀wal 1333   = wceq 1335  [wsb 1742   ∈ wcel 2128  {cab 2143  [wsbc 2937  ⦋csb 3031 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-11 1486  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139 This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-sbc 2938  df-csb 3032 This theorem is referenced by:  zproddc  11458  fprodseq  11462
 Copyright terms: Public domain W3C validator