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

Theorem csbcow 3069
Description: Composition law for chained substitutions into a class. Version of csbco 3068 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 3059 . . . . . 6 𝑦 / 𝑥𝐵 = {𝑧[𝑦 / 𝑥]𝑧𝐵}
21abeq2i 2288 . . . . 5 (𝑧𝑦 / 𝑥𝐵[𝑦 / 𝑥]𝑧𝐵)
32sbcbii 3023 . . . 4 ([𝐴 / 𝑦]𝑧𝑦 / 𝑥𝐵[𝐴 / 𝑦][𝑦 / 𝑥]𝑧𝐵)
4 nfv 1528 . . . . . . . . . 10 𝑦𝑥(𝑥 = 𝑤𝑧𝐵)
5 equequ2 1713 . . . . . . . . . . . 12 (𝑦 = 𝑤 → (𝑥 = 𝑦𝑥 = 𝑤))
65imbi1d 231 . . . . . . . . . . 11 (𝑦 = 𝑤 → ((𝑥 = 𝑦𝑧𝐵) ↔ (𝑥 = 𝑤𝑧𝐵)))
76albidv 1824 . . . . . . . . . 10 (𝑦 = 𝑤 → (∀𝑥(𝑥 = 𝑦𝑧𝐵) ↔ ∀𝑥(𝑥 = 𝑤𝑧𝐵)))
84, 7sbiev 1792 . . . . . . . . 9 ([𝑤 / 𝑦]∀𝑥(𝑥 = 𝑦𝑧𝐵) ↔ ∀𝑥(𝑥 = 𝑤𝑧𝐵))
9 sb6 1886 . . . . . . . . 9 ([𝑤 / 𝑥]𝑧𝐵 ↔ ∀𝑥(𝑥 = 𝑤𝑧𝐵))
108, 9bitr4i 187 . . . . . . . 8 ([𝑤 / 𝑦]∀𝑥(𝑥 = 𝑦𝑧𝐵) ↔ [𝑤 / 𝑥]𝑧𝐵)
11 df-clab 2164 . . . . . . . 8 (𝑤 ∈ {𝑦 ∣ ∀𝑥(𝑥 = 𝑦𝑧𝐵)} ↔ [𝑤 / 𝑦]∀𝑥(𝑥 = 𝑦𝑧𝐵))
12 df-clab 2164 . . . . . . . 8 (𝑤 ∈ {𝑥𝑧𝐵} ↔ [𝑤 / 𝑥]𝑧𝐵)
1310, 11, 123bitr4i 212 . . . . . . 7 (𝑤 ∈ {𝑦 ∣ ∀𝑥(𝑥 = 𝑦𝑧𝐵)} ↔ 𝑤 ∈ {𝑥𝑧𝐵})
1413eqriv 2174 . . . . . 6 {𝑦 ∣ ∀𝑥(𝑥 = 𝑦𝑧𝐵)} = {𝑥𝑧𝐵}
1514eleq2i 2244 . . . . 5 (𝐴 ∈ {𝑦 ∣ ∀𝑥(𝑥 = 𝑦𝑧𝐵)} ↔ 𝐴 ∈ {𝑥𝑧𝐵})
16 df-sbc 2964 . . . . . 6 ([𝐴 / 𝑦][𝑦 / 𝑥]𝑧𝐵𝐴 ∈ {𝑦[𝑦 / 𝑥]𝑧𝐵})
17 df-sbc 2964 . . . . . . . . 9 ([𝑦 / 𝑥]𝑧𝐵𝑦 ∈ {𝑥𝑧𝐵})
18 df-clab 2164 . . . . . . . . . 10 (𝑦 ∈ {𝑥𝑧𝐵} ↔ [𝑦 / 𝑥]𝑧𝐵)
19 sb6 1886 . . . . . . . . . 10 ([𝑦 / 𝑥]𝑧𝐵 ↔ ∀𝑥(𝑥 = 𝑦𝑧𝐵))
2018, 19bitri 184 . . . . . . . . 9 (𝑦 ∈ {𝑥𝑧𝐵} ↔ ∀𝑥(𝑥 = 𝑦𝑧𝐵))
2117, 20bitri 184 . . . . . . . 8 ([𝑦 / 𝑥]𝑧𝐵 ↔ ∀𝑥(𝑥 = 𝑦𝑧𝐵))
2221abbii 2293 . . . . . . 7 {𝑦[𝑦 / 𝑥]𝑧𝐵} = {𝑦 ∣ ∀𝑥(𝑥 = 𝑦𝑧𝐵)}
2322eleq2i 2244 . . . . . 6 (𝐴 ∈ {𝑦[𝑦 / 𝑥]𝑧𝐵} ↔ 𝐴 ∈ {𝑦 ∣ ∀𝑥(𝑥 = 𝑦𝑧𝐵)})
2416, 23bitri 184 . . . . 5 ([𝐴 / 𝑦][𝑦 / 𝑥]𝑧𝐵𝐴 ∈ {𝑦 ∣ ∀𝑥(𝑥 = 𝑦𝑧𝐵)})
25 df-sbc 2964 . . . . 5 ([𝐴 / 𝑥]𝑧𝐵𝐴 ∈ {𝑥𝑧𝐵})
2615, 24, 253bitr4i 212 . . . 4 ([𝐴 / 𝑦][𝑦 / 𝑥]𝑧𝐵[𝐴 / 𝑥]𝑧𝐵)
273, 26bitri 184 . . 3 ([𝐴 / 𝑦]𝑧𝑦 / 𝑥𝐵[𝐴 / 𝑥]𝑧𝐵)
2827abbii 2293 . 2 {𝑧[𝐴 / 𝑦]𝑧𝑦 / 𝑥𝐵} = {𝑧[𝐴 / 𝑥]𝑧𝐵}
29 df-csb 3059 . 2 𝐴 / 𝑦𝑦 / 𝑥𝐵 = {𝑧[𝐴 / 𝑦]𝑧𝑦 / 𝑥𝐵}
30 df-csb 3059 . 2 𝐴 / 𝑥𝐵 = {𝑧[𝐴 / 𝑥]𝑧𝐵}
3128, 29, 303eqtr4i 2208 1 𝐴 / 𝑦𝑦 / 𝑥𝐵 = 𝐴 / 𝑥𝐵
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1351   = wceq 1353  [wsb 1762  wcel 2148  {cab 2163  [wsbc 2963  csb 3058
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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-sbc 2964  df-csb 3059
This theorem is referenced by:  zproddc  11587  fprodseq  11591
  Copyright terms: Public domain W3C validator