Theorem csbxp 5753

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.

Step	Hyp	Ref	Expression
1		csbab 4397	. . 3 ⊢ ⦋𝐴 / 𝑥⦌{𝑧 ∣ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))} = {𝑧 ∣ [𝐴 / 𝑥]∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))}
2		sbcex2 3807	. . . . 5 ⊢ ([𝐴 / 𝑥]∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑤[𝐴 / 𝑥]∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
3		sbcex2 3807	. . . . . . 7 ⊢ ([𝐴 / 𝑥]∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑦[𝐴 / 𝑥](𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
4		sbcan 3796	. . . . . . . . 9 ⊢ ([𝐴 / 𝑥](𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ([𝐴 / 𝑥]𝑧 = ⟨𝑤, 𝑦⟩ ∧ [𝐴 / 𝑥](𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
5		sbcg 3819	. . . . . . . . . . 11 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑥]𝑧 = ⟨𝑤, 𝑦⟩ ↔ 𝑧 = ⟨𝑤, 𝑦⟩))
6		sbcan 3796	. . . . . . . . . . . . 13 ⊢ ([𝐴 / 𝑥](𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ↔ ([𝐴 / 𝑥]𝑤 ∈ 𝐵 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐶))
7		sbcel2 4375	. . . . . . . . . . . . . 14 ⊢ ([𝐴 / 𝑥]𝑤 ∈ 𝐵 ↔ 𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵)
8		sbcel2 4375	. . . . . . . . . . . . . 14 ⊢ ([𝐴 / 𝑥]𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)
9	7, 8	anbi12i 639	. . . . . . . . . . . . 13 ⊢ (([𝐴 / 𝑥]𝑤 ∈ 𝐵 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐶) ↔ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))
10	6, 9	bitri 278	. . . . . . . . . . . 12 ⊢ ([𝐴 / 𝑥](𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ↔ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))
11	10	a1i 11	. . . . . . . . . . 11 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑥](𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ↔ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)))
12	5, 11	anbi12d 643	. . . . . . . . . 10 ⊢ (𝐴 ∈ V → (([𝐴 / 𝑥]𝑧 = ⟨𝑤, 𝑦⟩ ∧ [𝐴 / 𝑥](𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))))
13		sbcex 3757	. . . . . . . . . . . . 13 ⊢ ([𝐴 / 𝑥](𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ V)
14	13	con3i 155	. . . . . . . . . . . 12 ⊢ (¬ 𝐴 ∈ V → ¬ [𝐴 / 𝑥](𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))
15	14	intnand 493	. . . . . . . . . . 11 ⊢ (¬ 𝐴 ∈ V → ¬ ([𝐴 / 𝑥]𝑧 = ⟨𝑤, 𝑦⟩ ∧ [𝐴 / 𝑥](𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
16		noel 4293	. . . . . . . . . . . . . . 15 ⊢ ¬ 𝑦 ∈ ∅
17	16	a1i 11	. . . . . . . . . . . . . 14 ⊢ (¬ 𝐴 ∈ V → ¬ 𝑦 ∈ ∅)
18		csbprc 4366	. . . . . . . . . . . . . 14 ⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐶 = ∅)
19	17, 18	neleqtrrd 2888	. . . . . . . . . . . . 13 ⊢ (¬ 𝐴 ∈ V → ¬ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)
20	19	intnand 493	. . . . . . . . . . . 12 ⊢ (¬ 𝐴 ∈ V → ¬ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))
21	20	intnand 493	. . . . . . . . . . 11 ⊢ (¬ 𝐴 ∈ V → ¬ (𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)))
22	15, 21	2falsed 379	. . . . . . . . . 10 ⊢ (¬ 𝐴 ∈ V → (([𝐴 / 𝑥]𝑧 = ⟨𝑤, 𝑦⟩ ∧ [𝐴 / 𝑥](𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))))
23	12, 22	pm2.61i 184	. . . . . . . . 9 ⊢ (([𝐴 / 𝑥]𝑧 = ⟨𝑤, 𝑦⟩ ∧ [𝐴 / 𝑥](𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)))
24	4, 23	bitri 278	. . . . . . . 8 ⊢ ([𝐴 / 𝑥](𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)))
25	24	exbii 1871	. . . . . . 7 ⊢ (∃𝑦[𝐴 / 𝑥](𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)))
26	3, 25	bitri 278	. . . . . 6 ⊢ ([𝐴 / 𝑥]∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)))
27	26	exbii 1871	. . . . 5 ⊢ (∃𝑤[𝐴 / 𝑥]∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)))
28	2, 27	bitri 278	. . . 4 ⊢ ([𝐴 / 𝑥]∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)))
29	28	abbii 2832	. . 3 ⊢ {𝑧 ∣ [𝐴 / 𝑥]∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))} = {𝑧 ∣ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))}
30	1, 29	eqtri 2788	. 2 ⊢ ⦋𝐴 / 𝑥⦌{𝑧 ∣ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))} = {𝑧 ∣ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))}
31		df-xp 5658	. . . 4 ⊢ (𝐵 × 𝐶) = {⟨𝑤, 𝑦⟩ ∣ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)}
32		df-opab 5168	. . . 4 ⊢ {⟨𝑤, 𝑦⟩ ∣ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)} = {𝑧 ∣ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))}
33	31, 32	eqtri 2788	. . 3 ⊢ (𝐵 × 𝐶) = {𝑧 ∣ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))}
34	33	csbeq2i 3863	. 2 ⊢ ⦋𝐴 / 𝑥⦌(𝐵 × 𝐶) = ⦋𝐴 / 𝑥⦌{𝑧 ∣ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))}
35		df-xp 5658	. . 3 ⊢ (⦋𝐴 / 𝑥⦌𝐵 × ⦋𝐴 / 𝑥⦌𝐶) = {⟨𝑤, 𝑦⟩ ∣ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)}
36		df-opab 5168	. . 3 ⊢ {⟨𝑤, 𝑦⟩ ∣ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)} = {𝑧 ∣ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))}
37	35, 36	eqtri 2788	. 2 ⊢ (⦋𝐴 / 𝑥⦌𝐵 × ⦋𝐴 / 𝑥⦌𝐶) = {𝑧 ∣ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))}
38	30, 34, 37	3eqtr4i 2798	1 ⊢ ⦋𝐴 / 𝑥⦌(𝐵 × 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 × ⦋𝐴 / 𝑥⦌𝐶)

Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 400   = wceq 1563  ∃wex 1802   ∈ wcel 2145  {cab 2743  Vcvv 3457  [wsbc 3747  ⦋csb 3855  ∅c0 4288  ⟨cop 4591  {copab 5167   × cxp 5650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-nul 4289  df-opab 5168  df-xp 5658

This theorem is referenced by:  csbres  5972  csbfinxpg  37894  csbresgVD  45468  disjxp1  45647