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

Theorem csbcow 3091
Description: Composition law for chained substitutions into a class. Version of csbco 3090 with a disjoint variable condition, which requires fewer axioms. (Contributed by NM, 10-Nov-2005.) (Revised by GG, 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 3081 . . . . . 6 𝑦 / 𝑥𝐵 = {𝑧[𝑦 / 𝑥]𝑧𝐵}
21abeq2i 2304 . . . . 5 (𝑧𝑦 / 𝑥𝐵[𝑦 / 𝑥]𝑧𝐵)
32sbcbii 3045 . . . 4 ([𝐴 / 𝑦]𝑧𝑦 / 𝑥𝐵[𝐴 / 𝑦][𝑦 / 𝑥]𝑧𝐵)
4 nfv 1539 . . . . . . . . . 10 𝑦𝑥(𝑥 = 𝑤𝑧𝐵)
5 equequ2 1724 . . . . . . . . . . . 12 (𝑦 = 𝑤 → (𝑥 = 𝑦𝑥 = 𝑤))
65imbi1d 231 . . . . . . . . . . 11 (𝑦 = 𝑤 → ((𝑥 = 𝑦𝑧𝐵) ↔ (𝑥 = 𝑤𝑧𝐵)))
76albidv 1835 . . . . . . . . . 10 (𝑦 = 𝑤 → (∀𝑥(𝑥 = 𝑦𝑧𝐵) ↔ ∀𝑥(𝑥 = 𝑤𝑧𝐵)))
84, 7sbiev 1803 . . . . . . . . 9 ([𝑤 / 𝑦]∀𝑥(𝑥 = 𝑦𝑧𝐵) ↔ ∀𝑥(𝑥 = 𝑤𝑧𝐵))
9 sb6 1898 . . . . . . . . 9 ([𝑤 / 𝑥]𝑧𝐵 ↔ ∀𝑥(𝑥 = 𝑤𝑧𝐵))
108, 9bitr4i 187 . . . . . . . 8 ([𝑤 / 𝑦]∀𝑥(𝑥 = 𝑦𝑧𝐵) ↔ [𝑤 / 𝑥]𝑧𝐵)
11 df-clab 2180 . . . . . . . 8 (𝑤 ∈ {𝑦 ∣ ∀𝑥(𝑥 = 𝑦𝑧𝐵)} ↔ [𝑤 / 𝑦]∀𝑥(𝑥 = 𝑦𝑧𝐵))
12 df-clab 2180 . . . . . . . 8 (𝑤 ∈ {𝑥𝑧𝐵} ↔ [𝑤 / 𝑥]𝑧𝐵)
1310, 11, 123bitr4i 212 . . . . . . 7 (𝑤 ∈ {𝑦 ∣ ∀𝑥(𝑥 = 𝑦𝑧𝐵)} ↔ 𝑤 ∈ {𝑥𝑧𝐵})
1413eqriv 2190 . . . . . 6 {𝑦 ∣ ∀𝑥(𝑥 = 𝑦𝑧𝐵)} = {𝑥𝑧𝐵}
1514eleq2i 2260 . . . . 5 (𝐴 ∈ {𝑦 ∣ ∀𝑥(𝑥 = 𝑦𝑧𝐵)} ↔ 𝐴 ∈ {𝑥𝑧𝐵})
16 df-sbc 2986 . . . . . 6 ([𝐴 / 𝑦][𝑦 / 𝑥]𝑧𝐵𝐴 ∈ {𝑦[𝑦 / 𝑥]𝑧𝐵})
17 df-sbc 2986 . . . . . . . . 9 ([𝑦 / 𝑥]𝑧𝐵𝑦 ∈ {𝑥𝑧𝐵})
18 df-clab 2180 . . . . . . . . . 10 (𝑦 ∈ {𝑥𝑧𝐵} ↔ [𝑦 / 𝑥]𝑧𝐵)
19 sb6 1898 . . . . . . . . . 10 ([𝑦 / 𝑥]𝑧𝐵 ↔ ∀𝑥(𝑥 = 𝑦𝑧𝐵))
2018, 19bitri 184 . . . . . . . . 9 (𝑦 ∈ {𝑥𝑧𝐵} ↔ ∀𝑥(𝑥 = 𝑦𝑧𝐵))
2117, 20bitri 184 . . . . . . . 8 ([𝑦 / 𝑥]𝑧𝐵 ↔ ∀𝑥(𝑥 = 𝑦𝑧𝐵))
2221abbii 2309 . . . . . . 7 {𝑦[𝑦 / 𝑥]𝑧𝐵} = {𝑦 ∣ ∀𝑥(𝑥 = 𝑦𝑧𝐵)}
2322eleq2i 2260 . . . . . 6 (𝐴 ∈ {𝑦[𝑦 / 𝑥]𝑧𝐵} ↔ 𝐴 ∈ {𝑦 ∣ ∀𝑥(𝑥 = 𝑦𝑧𝐵)})
2416, 23bitri 184 . . . . 5 ([𝐴 / 𝑦][𝑦 / 𝑥]𝑧𝐵𝐴 ∈ {𝑦 ∣ ∀𝑥(𝑥 = 𝑦𝑧𝐵)})
25 df-sbc 2986 . . . . 5 ([𝐴 / 𝑥]𝑧𝐵𝐴 ∈ {𝑥𝑧𝐵})
2615, 24, 253bitr4i 212 . . . 4 ([𝐴 / 𝑦][𝑦 / 𝑥]𝑧𝐵[𝐴 / 𝑥]𝑧𝐵)
273, 26bitri 184 . . 3 ([𝐴 / 𝑦]𝑧𝑦 / 𝑥𝐵[𝐴 / 𝑥]𝑧𝐵)
2827abbii 2309 . 2 {𝑧[𝐴 / 𝑦]𝑧𝑦 / 𝑥𝐵} = {𝑧[𝐴 / 𝑥]𝑧𝐵}
29 df-csb 3081 . 2 𝐴 / 𝑦𝑦 / 𝑥𝐵 = {𝑧[𝐴 / 𝑦]𝑧𝑦 / 𝑥𝐵}
30 df-csb 3081 . 2 𝐴 / 𝑥𝐵 = {𝑧[𝐴 / 𝑥]𝑧𝐵}
3128, 29, 303eqtr4i 2224 1 𝐴 / 𝑦𝑦 / 𝑥𝐵 = 𝐴 / 𝑥𝐵
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1362   = wceq 1364  [wsb 1773  wcel 2164  {cab 2179  [wsbc 2985  csb 3080
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175
This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-sbc 2986  df-csb 3081
This theorem is referenced by:  zproddc  11722  fprodseq  11726
  Copyright terms: Public domain W3C validator