Theorem coundi

Description: Class composition distributes over union. (Contributed by NM, 21-Dec-2008) (Proof shortened by Andrew Salmon, 27-Aug-2011)

	Ref	Expression
Assertion	coundi	$$⊢A\circ \left(B\cup C\right)=\left(A\circ B\right)\cup \left(A\circ C\right)$$

Proof

Step	Hyp	Ref	Expression
1		unopab	$$⊢\left\{⟨x,y⟩|\exists z\left(xBz\wedge zAy\right)\right\}\cup \left\{⟨x,y⟩|\exists z\left(xCz\wedge zAy\right)\right\}=\left\{⟨x,y⟩|\left(\exists z\left(xBz\wedge zAy\right)\vee \exists z\left(xCz\wedge zAy\right)\right)\right\}$$
2		brun	$$⊢x\left(B\cup C\right)z\leftrightarrow \left(xBz\vee xCz\right)$$
3	2	anbi1i	$$⊢\left(x\left(B\cup C\right)z\wedge zAy\right)\leftrightarrow \left(\left(xBz\vee xCz\right)\wedge zAy\right)$$
4		andir	$$⊢\left(\left(xBz\vee xCz\right)\wedge zAy\right)\leftrightarrow \left(\left(xBz\wedge zAy\right)\vee \left(xCz\wedge zAy\right)\right)$$
5	3 4	bitri	$$⊢\left(x\left(B\cup C\right)z\wedge zAy\right)\leftrightarrow \left(\left(xBz\wedge zAy\right)\vee \left(xCz\wedge zAy\right)\right)$$
6	5	exbii	$$⊢\exists z\left(x\left(B\cup C\right)z\wedge zAy\right)\leftrightarrow \exists z\left(\left(xBz\wedge zAy\right)\vee \left(xCz\wedge zAy\right)\right)$$
7		19.43	$$⊢\exists z\left(\left(xBz\wedge zAy\right)\vee \left(xCz\wedge zAy\right)\right)\leftrightarrow \left(\exists z\left(xBz\wedge zAy\right)\vee \exists z\left(xCz\wedge zAy\right)\right)$$
8	6 7	bitr2i	$$⊢\left(\exists z\left(xBz\wedge zAy\right)\vee \exists z\left(xCz\wedge zAy\right)\right)\leftrightarrow \exists z\left(x\left(B\cup C\right)z\wedge zAy\right)$$
9	8	opabbii	$$⊢\left\{⟨x,y⟩|\left(\exists z\left(xBz\wedge zAy\right)\vee \exists z\left(xCz\wedge zAy\right)\right)\right\}=\left\{⟨x,y⟩|\exists z\left(x\left(B\cup C\right)z\wedge zAy\right)\right\}$$
10	1 9	eqtri	$$⊢\left\{⟨x,y⟩|\exists z\left(xBz\wedge zAy\right)\right\}\cup \left\{⟨x,y⟩|\exists z\left(xCz\wedge zAy\right)\right\}=\left\{⟨x,y⟩|\exists z\left(x\left(B\cup C\right)z\wedge zAy\right)\right\}$$
11		df-co	$$⊢A\circ B=\left\{⟨x,y⟩|\exists z\left(xBz\wedge zAy\right)\right\}$$
12		df-co	$$⊢A\circ C=\left\{⟨x,y⟩|\exists z\left(xCz\wedge zAy\right)\right\}$$
13	11 12	uneq12i	$$⊢\left(A\circ B\right)\cup \left(A\circ C\right)=\left\{⟨x,y⟩|\exists z\left(xBz\wedge zAy\right)\right\}\cup \left\{⟨x,y⟩|\exists z\left(xCz\wedge zAy\right)\right\}$$
14		df-co	$$⊢A\circ \left(B\cup C\right)=\left\{⟨x,y⟩|\exists z\left(x\left(B\cup C\right)z\wedge zAy\right)\right\}$$
15	10 13 14	3eqtr4ri	$$⊢A\circ \left(B\cup C\right)=\left(A\circ B\right)\cup \left(A\circ C\right)$$