Theorem csbingVD

Description: Virtual deduction proof of csbin . 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. csbin is csbingVD without virtual deductions and was automatically derived from csbingVD .

	Ref	Expression
Assertion	csbingVD	$$⊢A\in B\to ⦋A/x⦌\left(C\cap D\right)=⦋A/x⦌C\cap ⦋A/x⦌D$$

Proof

Step	Hyp	Ref	Expression
1		idn1	$$⊢\left(A\in B\to A\in B\right)$$
2		df-in	$$⊢C\cap D=\left\{y|\left(y\in C\wedge y\in D\right)\right\}$$
3	2	ax-gen	$$⊢\forall xC\cap D=\left\{y|\left(y\in C\wedge y\in D\right)\right\}$$
4		spsbc	$$⊢A\in B\to \left(\forall xC\cap D=\left\{y|\left(y\in C\wedge y\in D\right)\right\}\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}C\cap D=\left\{y|\left(y\in C\wedge y\in D\right)\right\}\right)$$
5	1 3 4	e10	$$⊢\left(A\in B\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}C\cap D=\left\{y|\left(y\in C\wedge y\in D\right)\right\}\right)$$
6		sbceqg	$$⊢A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}C\cap D=\left\{y|\left(y\in C\wedge y\in D\right)\right\}\leftrightarrow ⦋A/x⦌\left(C\cap D\right)=⦋A/x⦌\left\{y|\left(y\in C\wedge y\in D\right)\right\}\right)$$
7	6	biimpd	$$⊢A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}C\cap D=\left\{y|\left(y\in C\wedge y\in D\right)\right\}\to ⦋A/x⦌\left(C\cap D\right)=⦋A/x⦌\left\{y|\left(y\in C\wedge y\in D\right)\right\}\right)$$
8	1 5 7	e11	$$⊢\left(A\in B\to ⦋A/x⦌\left(C\cap D\right)=⦋A/x⦌\left\{y|\left(y\in C\wedge y\in D\right)\right\}\right)$$
9		csbab	$$⊢⦋A/x⦌\left\{y|\left(y\in C\wedge y\in D\right)\right\}=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\wedge y\in D\right)\right\}$$
10	9	a1i	$$⊢A\in B\to ⦋A/x⦌\left\{y|\left(y\in C\wedge y\in D\right)\right\}=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\wedge y\in D\right)\right\}$$
11	1 10	e1a	$$⊢\left(A\in B\to ⦋A/x⦌\left\{y|\left(y\in C\wedge y\in D\right)\right\}=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\wedge y\in D\right)\right\}\right)$$
12		eqeq1	$$⊢⦋A/x⦌\left(C\cap D\right)=⦋A/x⦌\left\{y|\left(y\in C\wedge y\in D\right)\right\}\to \left(⦋A/x⦌\left(C\cap D\right)=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\wedge y\in D\right)\right\}\leftrightarrow ⦋A/x⦌\left\{y|\left(y\in C\wedge y\in D\right)\right\}=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\wedge y\in D\right)\right\}\right)$$
13	12	biimprd	$$⊢⦋A/x⦌\left(C\cap D\right)=⦋A/x⦌\left\{y|\left(y\in C\wedge y\in D\right)\right\}\to \left(⦋A/x⦌\left\{y|\left(y\in C\wedge y\in D\right)\right\}=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\wedge y\in D\right)\right\}\to ⦋A/x⦌\left(C\cap D\right)=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\wedge y\in D\right)\right\}\right)$$
14	8 11 13	e11	$$⊢\left(A\in B\to ⦋A/x⦌\left(C\cap D\right)=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\wedge y\in D\right)\right\}\right)$$
15		sbcan	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\wedge y\in D\right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in D\right)$$
16	15	a1i	$$⊢A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\wedge y\in D\right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in D\right)\right)$$
17	1 16	e1a	$$⊢\left(A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\wedge y\in D\right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in D\right)\right)\right)$$
18		sbcel2	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\leftrightarrow y\in ⦋A/x⦌C$$
19	18	a1i	$$⊢A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\leftrightarrow y\in ⦋A/x⦌C\right)$$
20	1 19	e1a	$$⊢\left(A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\leftrightarrow y\in ⦋A/x⦌C\right)\right)$$
21		sbcel2	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in D\leftrightarrow y\in ⦋A/x⦌D$$
22	21	a1i	$$⊢A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in D\leftrightarrow y\in ⦋A/x⦌D\right)$$
23	1 22	e1a	$$⊢\left(A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in D\leftrightarrow y\in ⦋A/x⦌D\right)\right)$$
24		pm4.38	$$⊢\left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\leftrightarrow y\in ⦋A/x⦌C\right)\wedge \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in D\leftrightarrow y\in ⦋A/x⦌D\right)\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in D\right)\leftrightarrow \left(y\in ⦋A/x⦌C\wedge y\in ⦋A/x⦌D\right)\right)$$
25	24	ex	$$⊢\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{}}{]}y\in D\leftrightarrow y\in ⦋A/x⦌D\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in D\right)\leftrightarrow \left(y\in ⦋A/x⦌C\wedge y\in ⦋A/x⦌D\right)\right)\right)$$
26	20 23 25	e11	$$⊢\left(A\in B\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in D\right)\leftrightarrow \left(y\in ⦋A/x⦌C\wedge y\in ⦋A/x⦌D\right)\right)\right)$$
27		bibi1	$$⊢\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\wedge y\in D\right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in D\right)\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\wedge y\in D\right)\leftrightarrow \left(y\in ⦋A/x⦌C\wedge y\in ⦋A/x⦌D\right)\right)\leftrightarrow \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in D\right)\leftrightarrow \left(y\in ⦋A/x⦌C\wedge y\in ⦋A/x⦌D\right)\right)\right)$$
28	27	biimprd	$$⊢\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\wedge y\in D\right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in D\right)\right)\to \left(\left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in D\right)\leftrightarrow \left(y\in ⦋A/x⦌C\wedge y\in ⦋A/x⦌D\right)\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\wedge y\in D\right)\leftrightarrow \left(y\in ⦋A/x⦌C\wedge y\in ⦋A/x⦌D\right)\right)\right)$$
29	17 26 28	e11	$$⊢\left(A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\wedge y\in D\right)\leftrightarrow \left(y\in ⦋A/x⦌C\wedge y\in ⦋A/x⦌D\right)\right)\right)$$
30	29	gen11	$$⊢\left(A\in B\to \forall y\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\wedge y\in D\right)\leftrightarrow \left(y\in ⦋A/x⦌C\wedge y\in ⦋A/x⦌D\right)\right)\right)$$
31		abbib	$$⊢\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\wedge y\in D\right)\right\}=\left\{y|\left(y\in ⦋A/x⦌C\wedge y\in ⦋A/x⦌D\right)\right\}\leftrightarrow \forall y\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\wedge y\in D\right)\leftrightarrow \left(y\in ⦋A/x⦌C\wedge y\in ⦋A/x⦌D\right)\right)$$
32	31	biimpri	$$⊢\forall y\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\wedge y\in D\right)\leftrightarrow \left(y\in ⦋A/x⦌C\wedge y\in ⦋A/x⦌D\right)\right)\to \left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\wedge y\in D\right)\right\}=\left\{y|\left(y\in ⦋A/x⦌C\wedge y\in ⦋A/x⦌D\right)\right\}$$
33	30 32	e1a	$$⊢\left(A\in B\to \left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\wedge y\in D\right)\right\}=\left\{y|\left(y\in ⦋A/x⦌C\wedge y\in ⦋A/x⦌D\right)\right\}\right)$$
34		eqeq1	$$⊢⦋A/x⦌\left(C\cap D\right)=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\wedge y\in D\right)\right\}\to \left(⦋A/x⦌\left(C\cap D\right)=\left\{y|\left(y\in ⦋A/x⦌C\wedge y\in ⦋A/x⦌D\right)\right\}\leftrightarrow \left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\wedge y\in D\right)\right\}=\left\{y|\left(y\in ⦋A/x⦌C\wedge y\in ⦋A/x⦌D\right)\right\}\right)$$
35	34	biimprd	$$⊢⦋A/x⦌\left(C\cap D\right)=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\wedge y\in D\right)\right\}\to \left(\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y\in C\wedge y\in D\right)\right\}=\left\{y|\left(y\in ⦋A/x⦌C\wedge y\in ⦋A/x⦌D\right)\right\}\to ⦋A/x⦌\left(C\cap D\right)=\left\{y|\left(y\in ⦋A/x⦌C\wedge y\in ⦋A/x⦌D\right)\right\}\right)$$
36	14 33 35	e11	$$⊢\left(A\in B\to ⦋A/x⦌\left(C\cap D\right)=\left\{y|\left(y\in ⦋A/x⦌C\wedge y\in ⦋A/x⦌D\right)\right\}\right)$$
37		df-in	$$⊢⦋A/x⦌C\cap ⦋A/x⦌D=\left\{y|\left(y\in ⦋A/x⦌C\wedge y\in ⦋A/x⦌D\right)\right\}$$
38		eqeq2	$$⊢⦋A/x⦌C\cap ⦋A/x⦌D=\left\{y|\left(y\in ⦋A/x⦌C\wedge y\in ⦋A/x⦌D\right)\right\}\to \left(⦋A/x⦌\left(C\cap D\right)=⦋A/x⦌C\cap ⦋A/x⦌D\leftrightarrow ⦋A/x⦌\left(C\cap D\right)=\left\{y|\left(y\in ⦋A/x⦌C\wedge y\in ⦋A/x⦌D\right)\right\}\right)$$
39	38	biimprcd	$$⊢⦋A/x⦌\left(C\cap D\right)=\left\{y|\left(y\in ⦋A/x⦌C\wedge y\in ⦋A/x⦌D\right)\right\}\to \left(⦋A/x⦌C\cap ⦋A/x⦌D=\left\{y|\left(y\in ⦋A/x⦌C\wedge y\in ⦋A/x⦌D\right)\right\}\to ⦋A/x⦌\left(C\cap D\right)=⦋A/x⦌C\cap ⦋A/x⦌D\right)$$
40	36 37 39	e10	$$⊢\left(A\in B\to ⦋A/x⦌\left(C\cap D\right)=⦋A/x⦌C\cap ⦋A/x⦌D\right)$$
41	40	in1	$$⊢A\in B\to ⦋A/x⦌\left(C\cap D\right)=⦋A/x⦌C\cap ⦋A/x⦌D$$