Theorem csbunigVD

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

	Ref	Expression
Assertion	csbunigVD	$$⊢A\in V\to ⦋A/x⦌\bigcup B=\bigcup ⦋A/x⦌B$$

Proof

Step	Hyp	Ref	Expression
1		idn1	$$⊢\left(A\in V\to A\in V\right)$$
2		sbcg	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in y\leftrightarrow z\in y\right)$$
3	1 2	e1a	$$⊢\left(A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in y\leftrightarrow z\in y\right)\right)$$
4		sbcel2	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\leftrightarrow y\in ⦋A/x⦌B$$
5	4	a1i	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\leftrightarrow y\in ⦋A/x⦌B\right)$$
6	1 5	e1a	$$⊢\left(A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\leftrightarrow y\in ⦋A/x⦌B\right)\right)$$
7		pm4.38	$$⊢\left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in y\leftrightarrow z\in y\right)\wedge \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\leftrightarrow y\in ⦋A/x⦌B\right)\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in y\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\right)\leftrightarrow \left(z\in y\wedge y\in ⦋A/x⦌B\right)\right)$$
8	7	ex	$$⊢\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in y\leftrightarrow z\in y\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\leftrightarrow y\in ⦋A/x⦌B\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in y\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\right)\leftrightarrow \left(z\in y\wedge y\in ⦋A/x⦌B\right)\right)\right)$$
9	3 6 8	e11	$$⊢\left(A\in V\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in y\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\right)\leftrightarrow \left(z\in y\wedge y\in ⦋A/x⦌B\right)\right)\right)$$
10		sbcan	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z\in y\wedge y\in B\right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in y\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\right)$$
11	10	a1i	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z\in y\wedge y\in B\right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in y\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\right)\right)$$
12	1 11	e1a	$$⊢\left(A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z\in y\wedge y\in B\right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in y\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\right)\right)\right)$$
13		bibi1	$$⊢\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z\in y\wedge y\in B\right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in y\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\right)\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z\in y\wedge y\in B\right)\leftrightarrow \left(z\in y\wedge y\in ⦋A/x⦌B\right)\right)\leftrightarrow \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in y\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\right)\leftrightarrow \left(z\in y\wedge y\in ⦋A/x⦌B\right)\right)\right)$$
14	13	biimprcd	$$⊢\left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in y\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\right)\leftrightarrow \left(z\in y\wedge y\in ⦋A/x⦌B\right)\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z\in y\wedge y\in B\right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in y\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\right)\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z\in y\wedge y\in B\right)\leftrightarrow \left(z\in y\wedge y\in ⦋A/x⦌B\right)\right)\right)$$
15	9 12 14	e11	$$⊢\left(A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z\in y\wedge y\in B\right)\leftrightarrow \left(z\in y\wedge y\in ⦋A/x⦌B\right)\right)\right)$$
16	15	gen11	$$⊢\left(A\in V\to \forall y\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z\in y\wedge y\in B\right)\leftrightarrow \left(z\in y\wedge y\in ⦋A/x⦌B\right)\right)\right)$$
17		exbi	$$⊢\forall y\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z\in y\wedge y\in B\right)\leftrightarrow \left(z\in y\wedge y\in ⦋A/x⦌B\right)\right)\to \left(\exists y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z\in y\wedge y\in B\right)\leftrightarrow \exists y\left(z\in y\wedge y\in ⦋A/x⦌B\right)\right)$$
18	16 17	e1a	$$⊢\left(A\in V\to \left(\exists y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z\in y\wedge y\in B\right)\leftrightarrow \exists y\left(z\in y\wedge y\in ⦋A/x⦌B\right)\right)\right)$$
19		sbcex2	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z\in y\wedge y\in B\right)\leftrightarrow \exists y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z\in y\wedge y\in B\right)$$
20	19	a1i	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z\in y\wedge y\in B\right)\leftrightarrow \exists y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z\in y\wedge y\in B\right)\right)$$
21	1 20	e1a	$$⊢\left(A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z\in y\wedge y\in B\right)\leftrightarrow \exists y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z\in y\wedge y\in B\right)\right)\right)$$
22		bibi1	$$⊢\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z\in y\wedge y\in B\right)\leftrightarrow \exists y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z\in y\wedge y\in B\right)\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z\in y\wedge y\in B\right)\leftrightarrow \exists y\left(z\in y\wedge y\in ⦋A/x⦌B\right)\right)\leftrightarrow \left(\exists y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z\in y\wedge y\in B\right)\leftrightarrow \exists y\left(z\in y\wedge y\in ⦋A/x⦌B\right)\right)\right)$$
23	22	biimprcd	$$⊢\left(\exists y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z\in y\wedge y\in B\right)\leftrightarrow \exists y\left(z\in y\wedge y\in ⦋A/x⦌B\right)\right)\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z\in y\wedge y\in B\right)\leftrightarrow \exists y\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(z\in y\wedge y\in B\right)\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z\in y\wedge y\in B\right)\leftrightarrow \exists y\left(z\in y\wedge y\in ⦋A/x⦌B\right)\right)\right)$$
24	18 21 23	e11	$$⊢\left(A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z\in y\wedge y\in B\right)\leftrightarrow \exists y\left(z\in y\wedge y\in ⦋A/x⦌B\right)\right)\right)$$
25	24	gen11	$$⊢\left(A\in V\to \forall z\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z\in y\wedge y\in B\right)\leftrightarrow \exists y\left(z\in y\wedge y\in ⦋A/x⦌B\right)\right)\right)$$
26		abbib	$$⊢\left\{z|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z\in y\wedge y\in B\right)\right\}=\left\{z|\exists y\left(z\in y\wedge y\in ⦋A/x⦌B\right)\right\}\leftrightarrow \forall z\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z\in y\wedge y\in B\right)\leftrightarrow \exists y\left(z\in y\wedge y\in ⦋A/x⦌B\right)\right)$$
27	26	biimpri	$$⊢\forall z\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z\in y\wedge y\in B\right)\leftrightarrow \exists y\left(z\in y\wedge y\in ⦋A/x⦌B\right)\right)\to \left\{z|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z\in y\wedge y\in B\right)\right\}=\left\{z|\exists y\left(z\in y\wedge y\in ⦋A/x⦌B\right)\right\}$$
28	25 27	e1a	$$⊢\left(A\in V\to \left\{z|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z\in y\wedge y\in B\right)\right\}=\left\{z|\exists y\left(z\in y\wedge y\in ⦋A/x⦌B\right)\right\}\right)$$
29		csbab	$$⊢⦋A/x⦌\left\{z|\exists y\left(z\in y\wedge y\in B\right)\right\}=\left\{z|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z\in y\wedge y\in B\right)\right\}$$
30	29	a1i	$$⊢A\in V\to ⦋A/x⦌\left\{z|\exists y\left(z\in y\wedge y\in B\right)\right\}=\left\{z|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z\in y\wedge y\in B\right)\right\}$$
31	1 30	e1a	$$⊢\left(A\in V\to ⦋A/x⦌\left\{z|\exists y\left(z\in y\wedge y\in B\right)\right\}=\left\{z|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z\in y\wedge y\in B\right)\right\}\right)$$
32		eqeq2	$$⊢\left\{z|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z\in y\wedge y\in B\right)\right\}=\left\{z|\exists y\left(z\in y\wedge y\in ⦋A/x⦌B\right)\right\}\to \left(⦋A/x⦌\left\{z|\exists y\left(z\in y\wedge y\in B\right)\right\}=\left\{z|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z\in y\wedge y\in B\right)\right\}\leftrightarrow ⦋A/x⦌\left\{z|\exists y\left(z\in y\wedge y\in B\right)\right\}=\left\{z|\exists y\left(z\in y\wedge y\in ⦋A/x⦌B\right)\right\}\right)$$
33	32	biimpd	$$⊢\left\{z|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z\in y\wedge y\in B\right)\right\}=\left\{z|\exists y\left(z\in y\wedge y\in ⦋A/x⦌B\right)\right\}\to \left(⦋A/x⦌\left\{z|\exists y\left(z\in y\wedge y\in B\right)\right\}=\left\{z|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(z\in y\wedge y\in B\right)\right\}\to ⦋A/x⦌\left\{z|\exists y\left(z\in y\wedge y\in B\right)\right\}=\left\{z|\exists y\left(z\in y\wedge y\in ⦋A/x⦌B\right)\right\}\right)$$
34	28 31 33	e11	$$⊢\left(A\in V\to ⦋A/x⦌\left\{z|\exists y\left(z\in y\wedge y\in B\right)\right\}=\left\{z|\exists y\left(z\in y\wedge y\in ⦋A/x⦌B\right)\right\}\right)$$
35		df-uni	$$⊢\bigcup B=\left\{z|\exists y\left(z\in y\wedge y\in B\right)\right\}$$
36	35	ax-gen	$$⊢\forall x\bigcup B=\left\{z|\exists y\left(z\in y\wedge y\in B\right)\right\}$$
37		spsbc	$$⊢A\in V\to \left(\forall x\bigcup B=\left\{z|\exists y\left(z\in y\wedge y\in B\right)\right\}\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\bigcup B=\left\{z|\exists y\left(z\in y\wedge y\in B\right)\right\}\right)$$
38	1 36 37	e10	$$⊢\left(A\in V\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\bigcup B=\left\{z|\exists y\left(z\in y\wedge y\in B\right)\right\}\right)$$
39		sbceqg	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\bigcup B=\left\{z|\exists y\left(z\in y\wedge y\in B\right)\right\}\leftrightarrow ⦋A/x⦌\bigcup B=⦋A/x⦌\left\{z|\exists y\left(z\in y\wedge y\in B\right)\right\}\right)$$
40	39	biimpd	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\bigcup B=\left\{z|\exists y\left(z\in y\wedge y\in B\right)\right\}\to ⦋A/x⦌\bigcup B=⦋A/x⦌\left\{z|\exists y\left(z\in y\wedge y\in B\right)\right\}\right)$$
41	1 38 40	e11	$$⊢\left(A\in V\to ⦋A/x⦌\bigcup B=⦋A/x⦌\left\{z|\exists y\left(z\in y\wedge y\in B\right)\right\}\right)$$
42		eqeq2	$$⊢⦋A/x⦌\left\{z|\exists y\left(z\in y\wedge y\in B\right)\right\}=\left\{z|\exists y\left(z\in y\wedge y\in ⦋A/x⦌B\right)\right\}\to \left(⦋A/x⦌\bigcup B=⦋A/x⦌\left\{z|\exists y\left(z\in y\wedge y\in B\right)\right\}\leftrightarrow ⦋A/x⦌\bigcup B=\left\{z|\exists y\left(z\in y\wedge y\in ⦋A/x⦌B\right)\right\}\right)$$
43	42	biimpd	$$⊢⦋A/x⦌\left\{z|\exists y\left(z\in y\wedge y\in B\right)\right\}=\left\{z|\exists y\left(z\in y\wedge y\in ⦋A/x⦌B\right)\right\}\to \left(⦋A/x⦌\bigcup B=⦋A/x⦌\left\{z|\exists y\left(z\in y\wedge y\in B\right)\right\}\to ⦋A/x⦌\bigcup B=\left\{z|\exists y\left(z\in y\wedge y\in ⦋A/x⦌B\right)\right\}\right)$$
44	34 41 43	e11	$$⊢\left(A\in V\to ⦋A/x⦌\bigcup B=\left\{z|\exists y\left(z\in y\wedge y\in ⦋A/x⦌B\right)\right\}\right)$$
45		df-uni	$$⊢\bigcup ⦋A/x⦌B=\left\{z|\exists y\left(z\in y\wedge y\in ⦋A/x⦌B\right)\right\}$$
46		eqeq2	$$⊢\bigcup ⦋A/x⦌B=\left\{z|\exists y\left(z\in y\wedge y\in ⦋A/x⦌B\right)\right\}\to \left(⦋A/x⦌\bigcup B=\bigcup ⦋A/x⦌B\leftrightarrow ⦋A/x⦌\bigcup B=\left\{z|\exists y\left(z\in y\wedge y\in ⦋A/x⦌B\right)\right\}\right)$$
47	46	biimprcd	$$⊢⦋A/x⦌\bigcup B=\left\{z|\exists y\left(z\in y\wedge y\in ⦋A/x⦌B\right)\right\}\to \left(\bigcup ⦋A/x⦌B=\left\{z|\exists y\left(z\in y\wedge y\in ⦋A/x⦌B\right)\right\}\to ⦋A/x⦌\bigcup B=\bigcup ⦋A/x⦌B\right)$$
48	44 45 47	e10	$$⊢\left(A\in V\to ⦋A/x⦌\bigcup B=\bigcup ⦋A/x⦌B\right)$$
49	48	in1	$$⊢A\in V\to ⦋A/x⦌\bigcup B=\bigcup ⦋A/x⦌B$$