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

Theorem csbxp 5234
Description: Distribute proper substitution through the Cartesian product of two classes. (Contributed by Alan Sare, 10-Nov-2012.) (Revised by NM, 23-Aug-2018.)
Assertion
Ref Expression
csbxp 𝐴 / 𝑥(𝐵 × 𝐶) = (𝐴 / 𝑥𝐵 × 𝐴 / 𝑥𝐶)

Proof of Theorem csbxp
Dummy variables 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 csbab 4041 . . 3 𝐴 / 𝑥{𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))} = {𝑧[𝐴 / 𝑥]𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))}
2 sbcex2 3519 . . . . 5 ([𝐴 / 𝑥]𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑤[𝐴 / 𝑥]𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)))
3 sbcex2 3519 . . . . . . 7 ([𝐴 / 𝑥]𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑦[𝐴 / 𝑥](𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)))
4 sbcan 3511 . . . . . . . . 9 ([𝐴 / 𝑥](𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ([𝐴 / 𝑥]𝑧 = ⟨𝑤, 𝑦⟩ ∧ [𝐴 / 𝑥](𝑤𝐵𝑦𝐶)))
5 sbcg 3536 . . . . . . . . . . 11 (𝐴 ∈ V → ([𝐴 / 𝑥]𝑧 = ⟨𝑤, 𝑦⟩ ↔ 𝑧 = ⟨𝑤, 𝑦⟩))
6 sbcan 3511 . . . . . . . . . . . . 13 ([𝐴 / 𝑥](𝑤𝐵𝑦𝐶) ↔ ([𝐴 / 𝑥]𝑤𝐵[𝐴 / 𝑥]𝑦𝐶))
7 sbcel2 4022 . . . . . . . . . . . . . 14 ([𝐴 / 𝑥]𝑤𝐵𝑤𝐴 / 𝑥𝐵)
8 sbcel2 4022 . . . . . . . . . . . . . 14 ([𝐴 / 𝑥]𝑦𝐶𝑦𝐴 / 𝑥𝐶)
97, 8anbi12i 733 . . . . . . . . . . . . 13 (([𝐴 / 𝑥]𝑤𝐵[𝐴 / 𝑥]𝑦𝐶) ↔ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))
106, 9bitri 264 . . . . . . . . . . . 12 ([𝐴 / 𝑥](𝑤𝐵𝑦𝐶) ↔ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))
1110a1i 11 . . . . . . . . . . 11 (𝐴 ∈ V → ([𝐴 / 𝑥](𝑤𝐵𝑦𝐶) ↔ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)))
125, 11anbi12d 747 . . . . . . . . . 10 (𝐴 ∈ V → (([𝐴 / 𝑥]𝑧 = ⟨𝑤, 𝑦⟩ ∧ [𝐴 / 𝑥](𝑤𝐵𝑦𝐶)) ↔ (𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))))
13 sbcex 3478 . . . . . . . . . . . . 13 ([𝐴 / 𝑥](𝑤𝐵𝑦𝐶) → 𝐴 ∈ V)
1413con3i 150 . . . . . . . . . . . 12 𝐴 ∈ V → ¬ [𝐴 / 𝑥](𝑤𝐵𝑦𝐶))
1514intnand 982 . . . . . . . . . . 11 𝐴 ∈ V → ¬ ([𝐴 / 𝑥]𝑧 = ⟨𝑤, 𝑦⟩ ∧ [𝐴 / 𝑥](𝑤𝐵𝑦𝐶)))
16 noel 3952 . . . . . . . . . . . . . . 15 ¬ 𝑦 ∈ ∅
1716a1i 11 . . . . . . . . . . . . . 14 𝐴 ∈ V → ¬ 𝑦 ∈ ∅)
18 csbprc 4013 . . . . . . . . . . . . . 14 𝐴 ∈ V → 𝐴 / 𝑥𝐶 = ∅)
1917, 18neleqtrrd 2752 . . . . . . . . . . . . 13 𝐴 ∈ V → ¬ 𝑦𝐴 / 𝑥𝐶)
2019intnand 982 . . . . . . . . . . . 12 𝐴 ∈ V → ¬ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))
2120intnand 982 . . . . . . . . . . 11 𝐴 ∈ V → ¬ (𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)))
2215, 212falsed 365 . . . . . . . . . 10 𝐴 ∈ V → (([𝐴 / 𝑥]𝑧 = ⟨𝑤, 𝑦⟩ ∧ [𝐴 / 𝑥](𝑤𝐵𝑦𝐶)) ↔ (𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))))
2312, 22pm2.61i 176 . . . . . . . . 9 (([𝐴 / 𝑥]𝑧 = ⟨𝑤, 𝑦⟩ ∧ [𝐴 / 𝑥](𝑤𝐵𝑦𝐶)) ↔ (𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)))
244, 23bitri 264 . . . . . . . 8 ([𝐴 / 𝑥](𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ (𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)))
2524exbii 1814 . . . . . . 7 (∃𝑦[𝐴 / 𝑥](𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)))
263, 25bitri 264 . . . . . 6 ([𝐴 / 𝑥]𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)))
2726exbii 1814 . . . . 5 (∃𝑤[𝐴 / 𝑥]𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)))
282, 27bitri 264 . . . 4 ([𝐴 / 𝑥]𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶)) ↔ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)))
2928abbii 2768 . . 3 {𝑧[𝐴 / 𝑥]𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))} = {𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))}
301, 29eqtri 2673 . 2 𝐴 / 𝑥{𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))} = {𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))}
31 df-xp 5149 . . . 4 (𝐵 × 𝐶) = {⟨𝑤, 𝑦⟩ ∣ (𝑤𝐵𝑦𝐶)}
32 df-opab 4746 . . . 4 {⟨𝑤, 𝑦⟩ ∣ (𝑤𝐵𝑦𝐶)} = {𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))}
3331, 32eqtri 2673 . . 3 (𝐵 × 𝐶) = {𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))}
3433csbeq2i 4026 . 2 𝐴 / 𝑥(𝐵 × 𝐶) = 𝐴 / 𝑥{𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐵𝑦𝐶))}
35 df-xp 5149 . . 3 (𝐴 / 𝑥𝐵 × 𝐴 / 𝑥𝐶) = {⟨𝑤, 𝑦⟩ ∣ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)}
36 df-opab 4746 . . 3 {⟨𝑤, 𝑦⟩ ∣ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶)} = {𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))}
3735, 36eqtri 2673 . 2 (𝐴 / 𝑥𝐵 × 𝐴 / 𝑥𝐶) = {𝑧 ∣ ∃𝑤𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤𝐴 / 𝑥𝐵𝑦𝐴 / 𝑥𝐶))}
3830, 34, 373eqtr4i 2683 1 𝐴 / 𝑥(𝐵 × 𝐶) = (𝐴 / 𝑥𝐵 × 𝐴 / 𝑥𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wa 383   = wceq 1523  wex 1744  wcel 2030  {cab 2637  Vcvv 3231  [wsbc 3468  csb 3566  c0 3948  cop 4216  {copab 4745   × cxp 5141
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-nul 3949  df-opab 4746  df-xp 5149
This theorem is referenced by:  csbres  5431  csbfinxpg  33355  csbresgOLD  39370  disjxp1  39552
  Copyright terms: Public domain W3C validator