Metamath Proof Explorer

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 (B \cup C) = (A \circ B) \cup (A \circ C)$

Proof

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