unrab

Description: Union of two restricted class abstractions. (Contributed by NM, 25-Mar-2004)

		Ref	Expression
	Assertion	unrab	$⊢ \{x \in A \| φ\} \cup \{x \in A \| ψ\} = \{x \in A \| (φ \lor ψ)\}$

Step	Hyp	Ref	Expression
1		df-rab	$⊢ \{x \in A \| φ\} = \{x \| (x \in A \land φ)\}$
2		df-rab	$⊢ \{x \in A \| ψ\} = \{x \| (x \in A \land ψ)\}$
3	1 2	uneq12i	$⊢ \{x \in A \| φ\} \cup \{x \in A \| ψ\} = \{x \| (x \in A \land φ)\} \cup \{x \| (x \in A \land ψ)\}$
4		df-rab	$⊢ \{x \in A \| (φ \lor ψ)\} = \{x \| (x \in A \land (φ \lor ψ))\}$
5		unab	$⊢ \{x \| (x \in A \land φ)\} \cup \{x \| (x \in A \land ψ)\} = \{x \| ((x \in A \land φ) \lor (x \in A \land ψ))\}$
6		andi	$⊢ (x \in A \land (φ \lor ψ)) \leftrightarrow ((x \in A \land φ) \lor (x \in A \land ψ))$
7	6	abbii	$⊢ \{x \| (x \in A \land (φ \lor ψ))\} = \{x \| ((x \in A \land φ) \lor (x \in A \land ψ))\}$
8	5 7	eqtr4i	$⊢ \{x \| (x \in A \land φ)\} \cup \{x \| (x \in A \land ψ)\} = \{x \| (x \in A \land (φ \lor ψ))\}$
9	4 8	eqtr4i	$⊢ \{x \in A \| (φ \lor ψ)\} = \{x \| (x \in A \land φ)\} \cup \{x \| (x \in A \land ψ)\}$
10	3 9	eqtr4i	$⊢ \{x \in A \| φ\} \cup \{x \in A \| ψ\} = \{x \in A \| (φ \lor ψ)\}$

Metamath Proof Explorer