Theorem sniota

Description: A class abstraction with a unique member can be expressed as a singleton. (Contributed by Mario Carneiro, 23-Dec-2016)

	Ref	Expression
Assertion	sniota	|- ( E! x ph -> { x | ph } = { ( iota x ph ) } )

Proof

Step	Hyp	Ref	Expression
1		nfeu1	|- F/ x E! x ph
2		nfab1	|- F/_ x { x | ph }
3		nfiota1	|- F/_ x ( iota x ph )
4	3	nfsn	|- F/_ x { ( iota x ph ) }
5		iota1	|- ( E! x ph -> ( ph <-> ( iota x ph ) = x ) )
6		eqcom	|- ( ( iota x ph ) = x <-> x = ( iota x ph ) )
7	5 6	bitrdi	|- ( E! x ph -> ( ph <-> x = ( iota x ph ) ) )
8		abid	|- ( x e. { x | ph } <-> ph )
9		velsn	|- ( x e. { ( iota x ph ) } <-> x = ( iota x ph ) )
10	7 8 9	3bitr4g	|- ( E! x ph -> ( x e. { x | ph } <-> x e. { ( iota x ph ) } ) )
11	1 2 4 10	eqrd	|- ( E! x ph -> { x | ph } = { ( iota x ph ) } )