rabun2

Description: Abstraction restricted to a union. (Contributed by Stefan O'Rear, 5-Feb-2015)

		Ref	Expression
	Assertion	rabun2	$⊢ \{x \in (A \cup B) \| φ\} = \{x \in A \| φ\} \cup \{x \in B \| φ\}$

Step	Hyp	Ref	Expression
1		df-rab	$⊢ \{x \in (A \cup B) \| φ\} = \{x \| (x \in (A \cup B) \land φ)\}$
2		df-rab	$⊢ \{x \in A \| φ\} = \{x \| (x \in A \land φ)\}$
3		df-rab	$⊢ \{x \in B \| φ\} = \{x \| (x \in B \land φ)\}$
4	2 3	uneq12i	$⊢ \{x \in A \| φ\} \cup \{x \in B \| φ\} = \{x \| (x \in A \land φ)\} \cup \{x \| (x \in B \land φ)\}$
5		elun	$⊢ x \in (A \cup B) \leftrightarrow (x \in A \lor x \in B)$
6	5	anbi1i	$⊢ (x \in (A \cup B) \land φ) \leftrightarrow ((x \in A \lor x \in B) \land φ)$
7		andir	$⊢ ((x \in A \lor x \in B) \land φ) \leftrightarrow ((x \in A \land φ) \lor (x \in B \land φ))$
8	6 7	bitri	$⊢ (x \in (A \cup B) \land φ) \leftrightarrow ((x \in A \land φ) \lor (x \in B \land φ))$
9	8	abbii	$⊢ \{x \| (x \in (A \cup B) \land φ)\} = \{x \| ((x \in A \land φ) \lor (x \in B \land φ))\}$
10		unab	$⊢ \{x \| (x \in A \land φ)\} \cup \{x \| (x \in B \land φ)\} = \{x \| ((x \in A \land φ) \lor (x \in B \land φ))\}$
11	9 10	eqtr4i	$⊢ \{x \| (x \in (A \cup B) \land φ)\} = \{x \| (x \in A \land φ)\} \cup \{x \| (x \in B \land φ)\}$
12	4 11	eqtr4i	$⊢ \{x \in A \| φ\} \cup \{x \in B \| φ\} = \{x \| (x \in (A \cup B) \land φ)\}$
13	1 12	eqtr4i	$⊢ \{x \in (A \cup B) \| φ\} = \{x \in A \| φ\} \cup \{x \in B \| φ\}$

Metamath Proof Explorer