Theorem csbxpgVD

Description: Virtual deduction proof of csbxp . The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. csbxp is csbxpgVD without virtual deductions and was automatically derived from csbxpgVD .

	Ref	Expression
Assertion	csbxpgVD	$$⊢A\in V\to ⦋A/x⦌\left(B\times C\right)=⦋A/x⦌B\times ⦋A/x⦌C$$

Proof

Step	Hyp	Ref	Expression
1		idn1	$$⊢\left(A\in V\to A\in V\right)$$
2		sbcel12	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}w\in B\leftrightarrow ⦋A/x⦌w\in ⦋A/x⦌B$$
3	2	a1i	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}w\in B\leftrightarrow ⦋A/x⦌w\in ⦋A/x⦌B\right)$$
4	1 3	e1a	$$⊢\left(A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}w\in B\leftrightarrow ⦋A/x⦌w\in ⦋A/x⦌B\right)\right)$$
5		csbconstg	$$⊢A\in V\to ⦋A/x⦌w=w$$
6	1 5	e1a	$$⊢\left(A\in V\to ⦋A/x⦌w=w\right)$$
7		eleq1	$$⊢⦋A/x⦌w=w\to \left(⦋A/x⦌w\in ⦋A/x⦌B\leftrightarrow w\in ⦋A/x⦌B\right)$$
8	6 7	e1a	$$⊢\left(A\in V\to \left(⦋A/x⦌w\in ⦋A/x⦌B\leftrightarrow w\in ⦋A/x⦌B\right)\right)$$
9		bibi1	$$⊢\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}w\in B\leftrightarrow ⦋A/x⦌w\in ⦋A/x⦌B\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}w\in B\leftrightarrow w\in ⦋A/x⦌B\right)\leftrightarrow \left(⦋A/x⦌w\in ⦋A/x⦌B\leftrightarrow w\in ⦋A/x⦌B\right)\right)$$
10	9	biimprd	$$⊢\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}w\in B\leftrightarrow ⦋A/x⦌w\in ⦋A/x⦌B\right)\to \left(\left(⦋A/x⦌w\in ⦋A/x⦌B\leftrightarrow w\in ⦋A/x⦌B\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}w\in B\leftrightarrow w\in ⦋A/x⦌B\right)\right)$$
11	4 8 10	e11	$$⊢\left(A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}w\in B\leftrightarrow w\in ⦋A/x⦌B\right)\right)$$
12		sbcel12	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\leftrightarrow ⦋A/x⦌y\in ⦋A/x⦌C$$
13	12	a1i	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\leftrightarrow ⦋A/x⦌y\in ⦋A/x⦌C\right)$$
14	1 13	e1a	$$⊢\left(A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\leftrightarrow ⦋A/x⦌y\in ⦋A/x⦌C\right)\right)$$
15		csbconstg	$$⊢A\in V\to ⦋A/x⦌y=y$$
16	1 15	e1a	$$⊢\left(A\in V\to ⦋A/x⦌y=y\right)$$
17		eleq1	$$⊢⦋A/x⦌y=y\to \left(⦋A/x⦌y\in ⦋A/x⦌C\leftrightarrow y\in ⦋A/x⦌C\right)$$
18	16 17	e1a	$$⊢\left(A\in V\to \left(⦋A/x⦌y\in ⦋A/x⦌C\leftrightarrow y\in ⦋A/x⦌C\right)\right)$$
19		bibi1	$$⊢\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\leftrightarrow ⦋A/x⦌y\in ⦋A/x⦌C\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\leftrightarrow y\in ⦋A/x⦌C\right)\leftrightarrow \left(⦋A/x⦌y\in ⦋A/x⦌C\leftrightarrow y\in ⦋A/x⦌C\right)\right)$$
20	19	biimprd	$$⊢\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\leftrightarrow ⦋A/x⦌y\in ⦋A/x⦌C\right)\to \left(\left(⦋A/x⦌y\in ⦋A/x⦌C\leftrightarrow y\in ⦋A/x⦌C\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\leftrightarrow y\in ⦋A/x⦌C\right)\right)$$
21	14 18 20	e11	$$⊢\left(A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\leftrightarrow y\in ⦋A/x⦌C\right)\right)$$
22		pm4.38	$$⊢\left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}w\in B\leftrightarrow w\in ⦋A/x⦌B\right)\wedge \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\leftrightarrow y\in ⦋A/x⦌C\right)\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}w\in B\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\right)\leftrightarrow \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)$$
23	22	ex	$$⊢\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}w\in B\leftrightarrow w\in ⦋A/x⦌B\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\leftrightarrow y\in ⦋A/x⦌C\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}w\in B\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\right)\leftrightarrow \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right)$$
24	11 21 23	e11	$$⊢\left(A\in V\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}w\in B\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\right)\leftrightarrow \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right)$$
25		sbcan	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(w\in B\wedge y\in C\right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}w\in B\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\right)$$
26	25	a1i	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(w\in B\wedge y\in C\right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}w\in B\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\right)\right)$$
27	1 26	e1a	$$⊢\left(A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(w\in B\wedge y\in C\right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}w\in B\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\right)\right)\right)$$
28		bibi1	$$⊢\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(w\in B\wedge y\in C\right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}w\in B\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\right)\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(w\in B\wedge y\in C\right)\leftrightarrow \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\leftrightarrow \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}w\in B\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\right)\leftrightarrow \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right)$$
29	28	biimprcd	$$⊢\left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}w\in B\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\right)\leftrightarrow \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(w\in B\wedge y\in C\right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}w\in B\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\right)\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(w\in B\wedge y\in C\right)\leftrightarrow \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right)$$
30	24 27 29	e11	$$⊢\left(A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(w\in B\wedge y\in C\right)\leftrightarrow \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right)$$
31		sbcg	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z=⟨w,y⟩\leftrightarrow z=⟨w,y⟩\right)$$
32	1 31	e1a	$$⊢\left(A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z=⟨w,y⟩\leftrightarrow z=⟨w,y⟩\right)\right)$$
33		pm4.38	$$⊢\left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z=⟨w,y⟩\leftrightarrow z=⟨w,y⟩\right)\wedge \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(w\in B\wedge y\in C\right)\leftrightarrow \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z=⟨w,y⟩\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(w\in B\wedge y\in C\right)\right)\leftrightarrow \left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right)$$
34	33	expcom	$$⊢\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(w\in B\wedge y\in C\right)\leftrightarrow \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z=⟨w,y⟩\leftrightarrow z=⟨w,y⟩\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z=⟨w,y⟩\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(w\in B\wedge y\in C\right)\right)\leftrightarrow \left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right)\right)$$
35	30 32 34	e11	$$⊢\left(A\in V\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z=⟨w,y⟩\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(w\in B\wedge y\in C\right)\right)\leftrightarrow \left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right)\right)$$
36		sbcan	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z=⟨w,y⟩\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(w\in B\wedge y\in C\right)\right)$$
37	36	a1i	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z=⟨w,y⟩\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(w\in B\wedge y\in C\right)\right)\right)$$
38	1 37	e1a	$$⊢\left(A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z=⟨w,y⟩\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(w\in B\wedge y\in C\right)\right)\right)\right)$$
39		bibi1	$$⊢\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z=⟨w,y⟩\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(w\in B\wedge y\in C\right)\right)\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right)\leftrightarrow \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z=⟨w,y⟩\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(w\in B\wedge y\in C\right)\right)\leftrightarrow \left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right)\right)$$
40	39	biimprcd	$$⊢\left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z=⟨w,y⟩\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(w\in B\wedge y\in C\right)\right)\leftrightarrow \left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z=⟨w,y⟩\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(w\in B\wedge y\in C\right)\right)\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right)\right)$$
41	35 38 40	e11	$$⊢\left(A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right)\right)$$
42	41	gen11	$$⊢\left(A\in V\to \forall y\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right)\right)$$
43		exbi	$$⊢\forall y\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right)\to \left(\exists y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \exists y\left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right)$$
44	42 43	e1a	$$⊢\left(A\in V\to \left(\exists y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \exists y\left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right)\right)$$
45		sbcex2	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \exists y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)$$
46	45	a1i	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \exists y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\right)$$
47	1 46	e1a	$$⊢\left(A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \exists y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\right)\right)$$
48		bibi1	$$⊢\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \exists y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \exists y\left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right)\leftrightarrow \left(\exists y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \exists y\left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right)\right)$$
49	48	biimprcd	$$⊢\left(\exists y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \exists y\left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \exists y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \exists y\left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right)\right)$$
50	44 47 49	e11	$$⊢\left(A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \exists y\left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right)\right)$$
51	50	gen11	$$⊢\left(A\in V\to \forall w\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \exists y\left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right)\right)$$
52		exbi	$$⊢\forall w\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \exists y\left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right)\to \left(\exists w\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right)$$
53	51 52	e1a	$$⊢\left(A\in V\to \left(\exists w\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right)\right)$$
54		sbcex2	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \exists w\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)$$
55	54	a1i	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \exists w\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\right)$$
56	1 55	e1a	$$⊢\left(A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \exists w\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\right)\right)$$
57		bibi1	$$⊢\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \exists w\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right)\leftrightarrow \left(\exists w\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right)\right)$$
58	57	biimprcd	$$⊢\left(\exists w\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \exists w\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right)\right)$$
59	53 56 58	e11	$$⊢\left(A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right)\right)$$
60	59	gen11	$$⊢\left(A\in V\to \forall z\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right)\right)$$
61		abbib	$$⊢\left\{z|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\right\}=\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right\}\leftrightarrow \forall z\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right)$$
62	61	biimpri	$$⊢\forall z\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\leftrightarrow \exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right)\to \left\{z|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\right\}=\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right\}$$
63	60 62	e1a	$$⊢\left(A\in V\to \left\{z|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\right\}=\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right\}\right)$$
64		csbab	$$⊢⦋A/x⦌\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\right\}=\left\{z|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\right\}$$
65	64	a1i	$$⊢A\in V\to ⦋A/x⦌\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\right\}=\left\{z|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\right\}$$
66	1 65	e1a	$$⊢\left(A\in V\to ⦋A/x⦌\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\right\}=\left\{z|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\right\}\right)$$
67		eqeq2	$$⊢\left\{z|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\right\}=\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right\}\to \left(⦋A/x⦌\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\right\}=\left\{z|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\right\}\leftrightarrow ⦋A/x⦌\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\right\}=\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right\}\right)$$
68	67	biimpd	$$⊢\left\{z|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\right\}=\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right\}\to \left(⦋A/x⦌\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\right\}=\left\{z|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\right\}\to ⦋A/x⦌\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\right\}=\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right\}\right)$$
69	63 66 68	e11	$$⊢\left(A\in V\to ⦋A/x⦌\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\right\}=\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right\}\right)$$
70		df-xp	$$⊢B\times C=\left\{⟨w,y⟩|\left(w\in B\wedge y\in C\right)\right\}$$
71		df-opab	$$⊢\left\{⟨w,y⟩|\left(w\in B\wedge y\in C\right)\right\}=\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\right\}$$
72	70 71	eqtri	$$⊢B\times C=\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\right\}$$
73	72	ax-gen	$$⊢\forall xB\times C=\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\right\}$$
74		csbeq2	$$⊢\forall xB\times C=\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\right\}\to ⦋A/x⦌\left(B\times C\right)=⦋A/x⦌\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\right\}$$
75	74	a1i	$$⊢A\in V\to \left(\forall xB\times C=\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\right\}\to ⦋A/x⦌\left(B\times C\right)=⦋A/x⦌\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\right\}\right)$$
76	1 73 75	e10	$$⊢\left(A\in V\to ⦋A/x⦌\left(B\times C\right)=⦋A/x⦌\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\right\}\right)$$
77		eqeq2	$$⊢⦋A/x⦌\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\right\}=\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right\}\to \left(⦋A/x⦌\left(B\times C\right)=⦋A/x⦌\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\right\}\leftrightarrow ⦋A/x⦌\left(B\times C\right)=\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right\}\right)$$
78	77	biimpd	$$⊢⦋A/x⦌\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\right\}=\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right\}\to \left(⦋A/x⦌\left(B\times C\right)=⦋A/x⦌\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in B\wedge y\in C\right)\right)\right\}\to ⦋A/x⦌\left(B\times C\right)=\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right\}\right)$$
79	69 76 78	e11	$$⊢\left(A\in V\to ⦋A/x⦌\left(B\times C\right)=\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right\}\right)$$
80		df-xp	$$⊢⦋A/x⦌B\times ⦋A/x⦌C=\left\{⟨w,y⟩|\left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right\}$$
81		df-opab	$$⊢\left\{⟨w,y⟩|\left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right\}=\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right\}$$
82	80 81	eqtri	$$⊢⦋A/x⦌B\times ⦋A/x⦌C=\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right\}$$
83		eqeq2	$$⊢⦋A/x⦌B\times ⦋A/x⦌C=\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right\}\to \left(⦋A/x⦌\left(B\times C\right)=⦋A/x⦌B\times ⦋A/x⦌C\leftrightarrow ⦋A/x⦌\left(B\times C\right)=\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right\}\right)$$
84	83	biimprcd	$$⊢⦋A/x⦌\left(B\times C\right)=\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right\}\to \left(⦋A/x⦌B\times ⦋A/x⦌C=\left\{z|\exists w\exists y\left(z=⟨w,y⟩\wedge \left(w\in ⦋A/x⦌B\wedge y\in ⦋A/x⦌C\right)\right)\right\}\to ⦋A/x⦌\left(B\times C\right)=⦋A/x⦌B\times ⦋A/x⦌C\right)$$
85	79 82 84	e10	$$⊢\left(A\in V\to ⦋A/x⦌\left(B\times C\right)=⦋A/x⦌B\times ⦋A/x⦌C\right)$$
86	85	in1	$$⊢A\in V\to ⦋A/x⦌\left(B\times C\right)=⦋A/x⦌B\times ⦋A/x⦌C$$