Theorem snriota

Description: A restricted class abstraction with a unique member can be expressed as a singleton. (Contributed by NM, 30-May-2006)

	Ref	Expression
Assertion	snriota	$$⊢\exists !x\in A\phi \to \left\{x\in A|\phi \right\}=\left\{\left(\iota x\in A|\phi \right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-reu	$$⊢\exists !x\in A\phi \leftrightarrow \exists !x\left(x\in A\wedge \phi \right)$$
2		sniota	$$⊢\exists !x\left(x\in A\wedge \phi \right)\to \left\{x|\left(x\in A\wedge \phi \right)\right\}=\left\{\left(\iota x|\left(x\in A\wedge \phi \right)\right)\right\}$$
3	1 2	sylbi	$$⊢\exists !x\in A\phi \to \left\{x|\left(x\in A\wedge \phi \right)\right\}=\left\{\left(\iota x|\left(x\in A\wedge \phi \right)\right)\right\}$$
4		df-rab	$$⊢\left\{x\in A|\phi \right\}=\left\{x|\left(x\in A\wedge \phi \right)\right\}$$
5		df-riota	$$⊢\left(\iota x\in A|\phi \right)=\left(\iota x|\left(x\in A\wedge \phi \right)\right)$$
6	5	sneqi	$$⊢\left\{\left(\iota x\in A|\phi \right)\right\}=\left\{\left(\iota x|\left(x\in A\wedge \phi \right)\right)\right\}$$
7	3 4 6	3eqtr4g	$$⊢\exists !x\in A\phi \to \left\{x\in A|\phi \right\}=\left\{\left(\iota x\in A|\phi \right)\right\}$$