riota1

Description: Property of restricted iota. Compare iota1 . (Contributed by Mario Carneiro, 15-Oct-2016)

		Ref	Expression
	Assertion	riota1	$⊢ \exists! x \in A φ \to ((x \in A \land φ) \leftrightarrow (ι x \in A \| φ) = x)$

Step	Hyp	Ref	Expression
1		df-reu	$⊢ \exists! x \in A φ \leftrightarrow \exists! x (x \in A \land φ)$
2		iota1	$⊢ \exists! x (x \in A \land φ) \to ((x \in A \land φ) \leftrightarrow (ι x \| (x \in A \land φ)) = x)$
3	1 2	sylbi	$⊢ \exists! x \in A φ \to ((x \in A \land φ) \leftrightarrow (ι x \| (x \in A \land φ)) = x)$
4		df-riota	$⊢ (ι x \in A \| φ) = (ι x \| (x \in A \land φ))$
5	4	eqeq1i	$⊢ (ι x \in A \| φ) = x \leftrightarrow (ι x \| (x \in A \land φ)) = x$
6	3 5	bitr4di	$⊢ \exists! x \in A φ \to ((x \in A \land φ) \leftrightarrow (ι x \in A \| φ) = x)$

Metamath Proof Explorer