Theorem csbxpg 4421

Description: Distribute proper substitution through the cross product of two classes. (Contributed by Alan Sare, 10-Nov-2012.)

Assertion

Ref	Expression
csbxpg	⊢ (𝐴 ∈ 𝐷 → ⦋𝐴 / 𝑥⦌(𝐵 × 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 × ⦋𝐴 / 𝑥⦌𝐶))

Proof of Theorem csbxpg

Dummy variables 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		csbabg 2907	. . 3 ⊢ (𝐴 ∈ 𝐷 → ⦋𝐴 / 𝑥⦌{𝑧 ∣ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))} = {𝑧 ∣ [𝐴 / 𝑥]∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))})
2		sbcexg 2813	. . . . 5 ⊢ (𝐴 ∈ 𝐷 → ([𝐴 / 𝑥]∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑤[𝐴 / 𝑥]∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))))
3		sbcexg 2813	. . . . . . 7 ⊢ (𝐴 ∈ 𝐷 → ([𝐴 / 𝑥]∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑦[𝐴 / 𝑥](𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))))
4		sbcang 2806	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝐷 → ([𝐴 / 𝑥](𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ([𝐴 / 𝑥]𝑧 = ⟨𝑤, 𝑦⟩ ∧ [𝐴 / 𝑥](𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))))
5		sbcg 2827	. . . . . . . . . 10 ⊢ (𝐴 ∈ 𝐷 → ([𝐴 / 𝑥]𝑧 = ⟨𝑤, 𝑦⟩ ↔ 𝑧 = ⟨𝑤, 𝑦⟩))
6		sbcang 2806	. . . . . . . . . . 11 ⊢ (𝐴 ∈ 𝐷 → ([𝐴 / 𝑥](𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ↔ ([𝐴 / 𝑥]𝑤 ∈ 𝐵 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐶)))
7		sbcel2g 2871	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ 𝐷 → ([𝐴 / 𝑥]𝑤 ∈ 𝐵 ↔ 𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵))
8		sbcel2g 2871	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ 𝐷 → ([𝐴 / 𝑥]𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))
9	7, 8	anbi12d 442	. . . . . . . . . . 11 ⊢ (𝐴 ∈ 𝐷 → (([𝐴 / 𝑥]𝑤 ∈ 𝐵 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐶) ↔ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)))
10	6, 9	bitrd 177	. . . . . . . . . 10 ⊢ (𝐴 ∈ 𝐷 → ([𝐴 / 𝑥](𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ↔ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)))
11	5, 10	anbi12d 442	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝐷 → (([𝐴 / 𝑥]𝑧 = ⟨𝑤, 𝑦⟩ ∧ [𝐴 / 𝑥](𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))))
12	4, 11	bitrd 177	. . . . . . . 8 ⊢ (𝐴 ∈ 𝐷 → ([𝐴 / 𝑥](𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))))
13	12	exbidv 1706	. . . . . . 7 ⊢ (𝐴 ∈ 𝐷 → (∃𝑦[𝐴 / 𝑥](𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))))
14	3, 13	bitrd 177	. . . . . 6 ⊢ (𝐴 ∈ 𝐷 → ([𝐴 / 𝑥]∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))))
15	14	exbidv 1706	. . . . 5 ⊢ (𝐴 ∈ 𝐷 → (∃𝑤[𝐴 / 𝑥]∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))))
16	2, 15	bitrd 177	. . . 4 ⊢ (𝐴 ∈ 𝐷 → ([𝐴 / 𝑥]∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))))
17	16	abbidv 2155	. . 3 ⊢ (𝐴 ∈ 𝐷 → {𝑧 ∣ [𝐴 / 𝑥]∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))} = {𝑧 ∣ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))})
18	1, 17	eqtrd 2072	. 2 ⊢ (𝐴 ∈ 𝐷 → ⦋𝐴 / 𝑥⦌{𝑧 ∣ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))} = {𝑧 ∣ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))})
19		df-xp 4351	. . . 4 ⊢ (𝐵 × 𝐶) = {⟨𝑤, 𝑦⟩ ∣ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)}
20		df-opab 3819	. . . 4 ⊢ {⟨𝑤, 𝑦⟩ ∣ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)} = {𝑧 ∣ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))}
21	19, 20	eqtri 2060	. . 3 ⊢ (𝐵 × 𝐶) = {𝑧 ∣ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))}
22	21	csbeq2i 2876	. 2 ⊢ ⦋𝐴 / 𝑥⦌(𝐵 × 𝐶) = ⦋𝐴 / 𝑥⦌{𝑧 ∣ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))}
23		df-xp 4351	. . 3 ⊢ (⦋𝐴 / 𝑥⦌𝐵 × ⦋𝐴 / 𝑥⦌𝐶) = {⟨𝑤, 𝑦⟩ ∣ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)}
24		df-opab 3819	. . 3 ⊢ {⟨𝑤, 𝑦⟩ ∣ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)} = {𝑧 ∣ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))}
25	23, 24	eqtri 2060	. 2 ⊢ (⦋𝐴 / 𝑥⦌𝐵 × ⦋𝐴 / 𝑥⦌𝐶) = {𝑧 ∣ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))}
26	18, 22, 25	3eqtr4g 2097	1 ⊢ (𝐴 ∈ 𝐷 → ⦋𝐴 / 𝑥⦌(𝐵 × 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 × ⦋𝐴 / 𝑥⦌𝐶))

Syntax hints:   → wi 4   ∧ wa 97   = wceq 1243  ∃wex 1381   ∈ wcel 1393  {cab 2026  [wsbc 2764  ⦋csb 2852  ⟨cop 3378  {copab 3817   × cxp 4343

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-v 2559  df-sbc 2765  df-csb 2853  df-opab 3819  df-xp 4351

This theorem is referenced by:  csbresg  4615