csbxp

Description: Distribute proper substitution through the Cartesian product of two classes. (Contributed by Alan Sare, 10-Nov-2012) (Revised by NM, 23-Aug-2018)

		Ref	Expression
	Assertion	csbxp	$⊢ ⦋ A / x ⦌ (B \times C) = ⦋ A / x ⦌ B \times ⦋ A / x ⦌ C$

Proof

Step	Hyp	Ref	Expression
1		csbab	$⊢ ⦋ A / x ⦌ \{z \| \exists w \exists y (z = ⟨w, y⟩ \land (w \in B \land y \in C))\} = \{z \| \underset{˙}{[} A / x \underset{˙}{]} \exists w \exists y (z = ⟨w, y⟩ \land (w \in B \land y \in C))\}$
2		sbcex2	$⊢ \underset{˙}{[} A / x \underset{˙}{]} \exists w \exists y (z = ⟨w, y⟩ \land (w \in B \land y \in C)) \leftrightarrow \exists w \underset{˙}{[} A / x \underset{˙}{]} \exists y (z = ⟨w, y⟩ \land (w \in B \land y \in C))$
3		sbcex2	$⊢ \underset{˙}{[} A / x \underset{˙}{]} \exists y (z = ⟨w, y⟩ \land (w \in B \land y \in C)) \leftrightarrow \exists y \underset{˙}{[} A / x \underset{˙}{]} (z = ⟨w, y⟩ \land (w \in B \land y \in C))$
4		sbcan	$⊢ \underset{˙}{[} A / x \underset{˙}{]} (z = ⟨w, y⟩ \land (w \in B \land y \in C)) \leftrightarrow (\underset{˙}{[} A / x \underset{˙}{]} z = ⟨w, y⟩ \land \underset{˙}{[} A / x \underset{˙}{]} (w \in B \land y \in C))$
5		sbcg	$⊢ A \in V \to (\underset{˙}{[} A / x \underset{˙}{]} z = ⟨w, y⟩ \leftrightarrow z = ⟨w, y⟩)$
6		sbcan	$⊢ \underset{˙}{[} A / x \underset{˙}{]} (w \in B \land y \in C) \leftrightarrow (\underset{˙}{[} A / x \underset{˙}{]} w \in B \land \underset{˙}{[} A / x \underset{˙}{]} y \in C)$
7		sbcel2	$⊢ \underset{˙}{[} A / x \underset{˙}{]} w \in B \leftrightarrow w \in ⦋ A / x ⦌ B$
8		sbcel2	$⊢ \underset{˙}{[} A / x \underset{˙}{]} y \in C \leftrightarrow y \in ⦋ A / x ⦌ C$
9	7 8	anbi12i	$⊢ (\underset{˙}{[} A / x \underset{˙}{]} w \in B \land \underset{˙}{[} A / x \underset{˙}{]} y \in C) \leftrightarrow (w \in ⦋ A / x ⦌ B \land y \in ⦋ A / x ⦌ C)$
10	6 9	bitri	$⊢ \underset{˙}{[} A / x \underset{˙}{]} (w \in B \land y \in C) \leftrightarrow (w \in ⦋ A / x ⦌ B \land y \in ⦋ A / x ⦌ C)$
11	10	a1i	$⊢ A \in V \to (\underset{˙}{[} A / x \underset{˙}{]} (w \in B \land y \in C) \leftrightarrow (w \in ⦋ A / x ⦌ B \land y \in ⦋ A / x ⦌ C))$
12	5 11	anbi12d	$⊢ A \in V \to ((\underset{˙}{[} A / x \underset{˙}{]} z = ⟨w, y⟩ \land \underset{˙}{[} A / x \underset{˙}{]} (w \in B \land y \in C)) \leftrightarrow (z = ⟨w, y⟩ \land (w \in ⦋ A / x ⦌ B \land y \in ⦋ A / x ⦌ C)))$
13		sbcex	$⊢ \underset{˙}{[} A / x \underset{˙}{]} (w \in B \land y \in C) \to A \in V$
14	13	con3i	$⊢ \neg A \in V \to \neg \underset{˙}{[} A / x \underset{˙}{]} (w \in B \land y \in C)$
15	14	intnand	$⊢ \neg A \in V \to \neg (\underset{˙}{[} A / x \underset{˙}{]} z = ⟨w, y⟩ \land \underset{˙}{[} A / x \underset{˙}{]} (w \in B \land y \in C))$
16		noel	$⊢ \neg y \in \emptyset$
17	16	a1i	$⊢ \neg A \in V \to \neg y \in \emptyset$
18		csbprc	$⊢ \neg A \in V \to ⦋ A / x ⦌ C = \emptyset$
19	17 18	neleqtrrd	$⊢ \neg A \in V \to \neg y \in ⦋ A / x ⦌ C$
20	19	intnand	$⊢ \neg A \in V \to \neg (w \in ⦋ A / x ⦌ B \land y \in ⦋ A / x ⦌ C)$
21	20	intnand	$⊢ \neg A \in V \to \neg (z = ⟨w, y⟩ \land (w \in ⦋ A / x ⦌ B \land y \in ⦋ A / x ⦌ C))$
22	15 21	2falsed	$⊢ \neg A \in V \to ((\underset{˙}{[} A / x \underset{˙}{]} z = ⟨w, y⟩ \land \underset{˙}{[} A / x \underset{˙}{]} (w \in B \land y \in C)) \leftrightarrow (z = ⟨w, y⟩ \land (w \in ⦋ A / x ⦌ B \land y \in ⦋ A / x ⦌ C)))$
23	12 22	pm2.61i	$⊢ (\underset{˙}{[} A / x \underset{˙}{]} z = ⟨w, y⟩ \land \underset{˙}{[} A / x \underset{˙}{]} (w \in B \land y \in C)) \leftrightarrow (z = ⟨w, y⟩ \land (w \in ⦋ A / x ⦌ B \land y \in ⦋ A / x ⦌ C))$
24	4 23	bitri	$⊢ \underset{˙}{[} A / x \underset{˙}{]} (z = ⟨w, y⟩ \land (w \in B \land y \in C)) \leftrightarrow (z = ⟨w, y⟩ \land (w \in ⦋ A / x ⦌ B \land y \in ⦋ A / x ⦌ C))$
25	24	exbii	$⊢ \exists y \underset{˙}{[} A / x \underset{˙}{]} (z = ⟨w, y⟩ \land (w \in B \land y \in C)) \leftrightarrow \exists y (z = ⟨w, y⟩ \land (w \in ⦋ A / x ⦌ B \land y \in ⦋ A / x ⦌ C))$
26	3 25	bitri	$⊢ \underset{˙}{[} A / x \underset{˙}{]} \exists y (z = ⟨w, y⟩ \land (w \in B \land y \in C)) \leftrightarrow \exists y (z = ⟨w, y⟩ \land (w \in ⦋ A / x ⦌ B \land y \in ⦋ A / x ⦌ C))$
27	26	exbii	$⊢ \exists w \underset{˙}{[} A / x \underset{˙}{]} \exists y (z = ⟨w, y⟩ \land (w \in B \land y \in C)) \leftrightarrow \exists w \exists y (z = ⟨w, y⟩ \land (w \in ⦋ A / x ⦌ B \land y \in ⦋ A / x ⦌ C))$
28	2 27	bitri	$⊢ \underset{˙}{[} A / x \underset{˙}{]} \exists w \exists y (z = ⟨w, y⟩ \land (w \in B \land y \in C)) \leftrightarrow \exists w \exists y (z = ⟨w, y⟩ \land (w \in ⦋ A / x ⦌ B \land y \in ⦋ A / x ⦌ C))$
29	28	abbii	$⊢ \{z \| \underset{˙}{[} A / x \underset{˙}{]} \exists w \exists y (z = ⟨w, y⟩ \land (w \in B \land y \in C))\} = \{z \| \exists w \exists y (z = ⟨w, y⟩ \land (w \in ⦋ A / x ⦌ B \land y \in ⦋ A / x ⦌ C))\}$
30	1 29	eqtri	$⊢ ⦋ A / x ⦌ \{z \| \exists w \exists y (z = ⟨w, y⟩ \land (w \in B \land y \in C))\} = \{z \| \exists w \exists y (z = ⟨w, y⟩ \land (w \in ⦋ A / x ⦌ B \land y \in ⦋ A / x ⦌ C))\}$
31		df-xp	$⊢ B \times C = \{⟨w, y⟩ \| (w \in B \land y \in C)\}$
32		df-opab	$⊢ \{⟨w, y⟩ \| (w \in B \land y \in C)\} = \{z \| \exists w \exists y (z = ⟨w, y⟩ \land (w \in B \land y \in C))\}$
33	31 32	eqtri	$⊢ B \times C = \{z \| \exists w \exists y (z = ⟨w, y⟩ \land (w \in B \land y \in C))\}$
34	33	csbeq2i	$⊢ ⦋ A / x ⦌ (B \times C) = ⦋ A / x ⦌ \{z \| \exists w \exists y (z = ⟨w, y⟩ \land (w \in B \land y \in C))\}$
35		df-xp	$⊢ ⦋ A / x ⦌ B \times ⦋ A / x ⦌ C = \{⟨w, y⟩ \| (w \in ⦋ A / x ⦌ B \land y \in ⦋ A / x ⦌ C)\}$
36		df-opab	$⊢ \{⟨w, y⟩ \| (w \in ⦋ A / x ⦌ B \land y \in ⦋ A / x ⦌ C)\} = \{z \| \exists w \exists y (z = ⟨w, y⟩ \land (w \in ⦋ A / x ⦌ B \land y \in ⦋ A / x ⦌ C))\}$
37	35 36	eqtri	$⊢ ⦋ A / x ⦌ B \times ⦋ A / x ⦌ C = \{z \| \exists w \exists y (z = ⟨w, y⟩ \land (w \in ⦋ A / x ⦌ B \land y \in ⦋ A / x ⦌ C))\}$
38	30 34 37	3eqtr4i	$⊢ ⦋ A / x ⦌ (B \times C) = ⦋ A / x ⦌ B \times ⦋ A / x ⦌ C$

Metamath Proof Explorer

Theorem csbxp

Proof