Theorem csbxp 5751

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 3798	. . . . 5 ⊢ ([𝐴 / 𝑥]∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑤[𝐴 / 𝑥]∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
3		sbcex2 3798	. . . . . . 7 ⊢ ([𝐴 / 𝑥]∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑦[𝐴 / 𝑥](𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
4		sbcan 3787	. . . . . . . . 9 ⊢ ([𝐴 / 𝑥](𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ([𝐴 / 𝑥]𝑧 = ⟨𝑤, 𝑦⟩ ∧ [𝐴 / 𝑥](𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
5		sbcg 3810	. . . . . . . . . . 11 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑥]𝑧 = ⟨𝑤, 𝑦⟩ ↔ 𝑧 = ⟨𝑤, 𝑦⟩))
6		sbcan 3787	. . . . . . . . . . . . 13 ⊢ ([𝐴 / 𝑥](𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ↔ ([𝐴 / 𝑥]𝑤 ∈ 𝐵 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐶))
7		sbcel2 4375	. . . . . . . . . . . . . 14 ⊢ ([𝐴 / 𝑥]𝑤 ∈ 𝐵 ↔ 𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵)
8		sbcel2 4375	. . . . . . . . . . . . . 14 ⊢ ([𝐴 / 𝑥]𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)
9	7, 8	anbi12i 640	. . . . . . . . . . . . 13 ⊢ (([𝐴 / 𝑥]𝑤 ∈ 𝐵 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐶) ↔ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))
10	6, 9	bitri 278	. . . . . . . . . . . 12 ⊢ ([𝐴 / 𝑥](𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ↔ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))
11	10	a1i 11	. . . . . . . . . . 11 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑥](𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ↔ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)))
12	5, 11	anbi12d 644	. . . . . . . . . 10 ⊢ (𝐴 ∈ V → (([𝐴 / 𝑥]𝑧 = ⟨𝑤, 𝑦⟩ ∧ [𝐴 / 𝑥](𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))))
13		sbcex 3748	. . . . . . . . . . . . 13 ⊢ ([𝐴 / 𝑥](𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ V)
14	13	con3i 155	. . . . . . . . . . . 12 ⊢ (¬ 𝐴 ∈ V → ¬ [𝐴 / 𝑥](𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))
15	14	intnand 494	. . . . . . . . . . 11 ⊢ (¬ 𝐴 ∈ V → ¬ ([𝐴 / 𝑥]𝑧 = ⟨𝑤, 𝑦⟩ ∧ [𝐴 / 𝑥](𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))
16		noel 4283	. . . . . . . . . . . . . . 15 ⊢ ¬ 𝑦 ∈ ∅
17	16	a1i 11	. . . . . . . . . . . . . 14 ⊢ (¬ 𝐴 ∈ V → ¬ 𝑦 ∈ ∅)
18		csbprc 4366	. . . . . . . . . . . . . 14 ⊢ (¬ 𝐴 ∈ V → ⦋𝐴 / 𝑥⦌𝐶 = ∅)
19	17, 18	neleqtrrd 2883	. . . . . . . . . . . . 13 ⊢ (¬ 𝐴 ∈ V → ¬ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)
20	19	intnand 494	. . . . . . . . . . . 12 ⊢ (¬ 𝐴 ∈ V → ¬ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))
21	20	intnand 494	. . . . . . . . . . 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 1880	. . . . . . 7 ⊢ (∃𝑦[𝐴 / 𝑥](𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)))
26	3, 25	bitri 278	. . . . . 6 ⊢ ([𝐴 / 𝑥]∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)))
27	26	exbii 1880	. . . . 5 ⊢ (∃𝑤[𝐴 / 𝑥]∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)))
28	2, 27	bitri 278	. . . 4 ⊢ ([𝐴 / 𝑥]∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)))
29	28	abbii 2827	. . 3 ⊢ {𝑧 ∣ [𝐴 / 𝑥]∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))} = {𝑧 ∣ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))}
30	1, 29	eqtri 2783	. 2 ⊢ ⦋𝐴 / 𝑥⦌{𝑧 ∣ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))} = {𝑧 ∣ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))}
31		df-xp 5656	. . . 4 ⊢ (𝐵 × 𝐶) = {⟨𝑤, 𝑦⟩ ∣ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)}
32		df-opab 5167	. . . 4 ⊢ {⟨𝑤, 𝑦⟩ ∣ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)} = {𝑧 ∣ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))}
33	31, 32	eqtri 2783	. . 3 ⊢ (𝐵 × 𝐶) = {𝑧 ∣ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))}
34	33	csbeq2i 3854	. 2 ⊢ ⦋𝐴 / 𝑥⦌(𝐵 × 𝐶) = ⦋𝐴 / 𝑥⦌{𝑧 ∣ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))}
35		df-xp 5656	. . 3 ⊢ (⦋𝐴 / 𝑥⦌𝐵 × ⦋𝐴 / 𝑥⦌𝐶) = {⟨𝑤, 𝑦⟩ ∣ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)}
36		df-opab 5167	. . 3 ⊢ {⟨𝑤, 𝑦⟩ ∣ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶)} = {𝑧 ∣ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))}
37	35, 36	eqtri 2783	. 2 ⊢ (⦋𝐴 / 𝑥⦌𝐵 × ⦋𝐴 / 𝑥⦌𝐶) = {𝑧 ∣ ∃𝑤∃𝑦(𝑧 = ⟨𝑤, 𝑦⟩ ∧ (𝑤 ∈ ⦋𝐴 / 𝑥⦌𝐵 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐶))}
38	30, 34, 37	3eqtr4i 2793	1 ⊢ ⦋𝐴 / 𝑥⦌(𝐵 × 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 × ⦋𝐴 / 𝑥⦌𝐶)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ∧ wa 401   = wceq 1569  ∃wex 1811   ∈ wcel 2144  {cab 2738  Vcvv 3450  [wsbc 3738  ⦋csb 3846  ∅c0 4278  ⟨cop 4834  {copab 5166   × cxp 5648

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-v 3452  df-sbc 3739  df-csb 3847  df-dif 4047  df-nul 4279  df-opab 5167  df-xp 5656

This theorem is used by:  csbres  5972  csbfinxpg  38404  csbresgVD  45970  disjxp1  46179