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	|- ( E! x e. A ph -> { x e. A | ph } = { ( iota_ x e. A ph ) } )

Proof

Step	Hyp	Ref	Expression
1		df-reu	|- ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )
2		sniota	|- ( E! x ( x e. A /\ ph ) -> { x | ( x e. A /\ ph ) } = { ( iota x ( x e. A /\ ph ) ) } )
3	1 2	sylbi	|- ( E! x e. A ph -> { x | ( x e. A /\ ph ) } = { ( iota x ( x e. A /\ ph ) ) } )
4		df-rab	|- { x e. A | ph } = { x | ( x e. A /\ ph ) }
5		df-riota	|- ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )
6	5	sneqi	|- { ( iota_ x e. A ph ) } = { ( iota x ( x e. A /\ ph ) ) }
7	3 4 6	3eqtr4g	|- ( E! x e. A ph -> { x e. A | ph } = { ( iota_ x e. A ph ) } )