Theorem csbuni

Description: Distribute proper substitution through the union of a class. (Contributed by Alan Sare, 10-Nov-2012) (Revised by NM, 22-Aug-2018)

	Ref	Expression
Assertion	csbuni	$$⊢⦋A/x⦌\bigcup B=\bigcup ⦋A/x⦌B$$

Proof

Step	Hyp	Ref	Expression
1		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\}$$
2		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)$$
3		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)$$
4		sbcg	$$⊢A\in \mathrm{V}\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in y\leftrightarrow z\in y\right)$$
5	4	anbi1d	$$⊢A\in \mathrm{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 \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\right)\right)$$
6		sbcel2	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\leftrightarrow y\in ⦋A/x⦌B$$
7	6	anbi2i	$$⊢\left(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)$$
8	5 7	bitrdi	$$⊢A\in \mathrm{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)$$
9	3 8	bitrid	$$⊢A\in \mathrm{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)$$
10	9	exbidv	$$⊢A\in \mathrm{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)$$
11	2 10	bitrid	$$⊢A\in \mathrm{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)$$
12	11	abbidv	$$⊢A\in \mathrm{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\}$$
13	1 12	eqtrid	$$⊢A\in \mathrm{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\}$$
14		df-uni	$$⊢\bigcup B=\left\{z|\exists y\left(z\in y\wedge y\in B\right)\right\}$$
15	14	csbeq2i	$$⊢⦋A/x⦌\bigcup B=⦋A/x⦌\left\{z|\exists y\left(z\in y\wedge y\in B\right)\right\}$$
16		df-uni	$$⊢\bigcup ⦋A/x⦌B=\left\{z|\exists y\left(z\in y\wedge y\in ⦋A/x⦌B\right)\right\}$$
17	13 15 16	3eqtr4g	$$⊢A\in \mathrm{V}\to ⦋A/x⦌\bigcup B=\bigcup ⦋A/x⦌B$$
18		csbprc	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌\bigcup B=\varnothing$$
19		csbprc	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌B=\varnothing$$
20	19	unieqd	$$⊢\neg A\in \mathrm{V}\to \bigcup ⦋A/x⦌B=\bigcup \varnothing$$
21		uni0	$$⊢\bigcup \varnothing =\varnothing$$
22	20 21	eqtr2di	$$⊢\neg A\in \mathrm{V}\to \varnothing =\bigcup ⦋A/x⦌B$$
23	18 22	eqtrd	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌\bigcup B=\bigcup ⦋A/x⦌B$$
24	17 23	pm2.61i	$$⊢⦋A/x⦌\bigcup B=\bigcup ⦋A/x⦌B$$