riota1a

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

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

Metamath Proof Explorer