riotauni

Description: Restricted iota in terms of class union. (Contributed by NM, 11-Oct-2011)

		Ref	Expression
	Assertion	riotauni	$⊢ \exists! x \in A φ \to (ι x \in A \| φ) = ⋃ \{x \in A \| φ\}$

Step	Hyp	Ref	Expression
1		df-reu	$⊢ \exists! x \in A φ \leftrightarrow \exists! x (x \in A \land φ)$
2		iotauni	$⊢ \exists! x (x \in A \land φ) \to (ι x \| (x \in A \land φ)) = ⋃ \{x \| (x \in A \land φ)\}$
3	1 2	sylbi	$⊢ \exists! x \in A φ \to (ι x \| (x \in A \land φ)) = ⋃ \{x \| (x \in A \land φ)\}$
4		df-riota	$⊢ (ι x \in A \| φ) = (ι x \| (x \in A \land φ))$
5		df-rab	$⊢ \{x \in A \| φ\} = \{x \| (x \in A \land φ)\}$
6	5	unieqi	$⊢ ⋃ \{x \in A \| φ\} = ⋃ \{x \| (x \in A \land φ)\}$
7	3 4 6	3eqtr4g	$⊢ \exists! x \in A φ \to (ι x \in A \| φ) = ⋃ \{x \in A \| φ\}$

Metamath Proof Explorer