mptun

Description: Union of mappings which are mutually compatible. (Contributed by Mario Carneiro, 31-Aug-2015)

		Ref	Expression
	Assertion	mptun	$⊢ (x \in (A \cup B) ⟼ C) = (x \in A ⟼ C) \cup (x \in B ⟼ C)$

Step	Hyp	Ref	Expression
1		df-mpt	$⊢ (x \in (A \cup B) ⟼ C) = \{⟨x, y⟩ \| (x \in (A \cup B) \land y = C)\}$
2		df-mpt	$⊢ (x \in A ⟼ C) = \{⟨x, y⟩ \| (x \in A \land y = C)\}$
3		df-mpt	$⊢ (x \in B ⟼ C) = \{⟨x, y⟩ \| (x \in B \land y = C)\}$
4	2 3	uneq12i	$⊢ (x \in A ⟼ C) \cup (x \in B ⟼ C) = \{⟨x, y⟩ \| (x \in A \land y = C)\} \cup \{⟨x, y⟩ \| (x \in B \land y = C)\}$
5		elun	$⊢ x \in (A \cup B) \leftrightarrow (x \in A \lor x \in B)$
6	5	anbi1i	$⊢ (x \in (A \cup B) \land y = C) \leftrightarrow ((x \in A \lor x \in B) \land y = C)$
7		andir	$⊢ ((x \in A \lor x \in B) \land y = C) \leftrightarrow ((x \in A \land y = C) \lor (x \in B \land y = C))$
8	6 7	bitri	$⊢ (x \in (A \cup B) \land y = C) \leftrightarrow ((x \in A \land y = C) \lor (x \in B \land y = C))$
9	8	opabbii	$⊢ \{⟨x, y⟩ \| (x \in (A \cup B) \land y = C)\} = \{⟨x, y⟩ \| ((x \in A \land y = C) \lor (x \in B \land y = C))\}$
10		unopab	$⊢ \{⟨x, y⟩ \| (x \in A \land y = C)\} \cup \{⟨x, y⟩ \| (x \in B \land y = C)\} = \{⟨x, y⟩ \| ((x \in A \land y = C) \lor (x \in B \land y = C))\}$
11	9 10	eqtr4i	$⊢ \{⟨x, y⟩ \| (x \in (A \cup B) \land y = C)\} = \{⟨x, y⟩ \| (x \in A \land y = C)\} \cup \{⟨x, y⟩ \| (x \in B \land y = C)\}$
12	4 11	eqtr4i	$⊢ (x \in A ⟼ C) \cup (x \in B ⟼ C) = \{⟨x, y⟩ \| (x \in (A \cup B) \land y = C)\}$
13	1 12	eqtr4i	$⊢ (x \in (A \cup B) ⟼ C) = (x \in A ⟼ C) \cup (x \in B ⟼ C)$

Metamath Proof Explorer