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	⊢ ( ∃! 𝑥 𝜑 → { 𝑥 ∣ 𝜑 } = { ( ℩ 𝑥 𝜑 ) } )

Proof

Step	Hyp	Ref	Expression
1		nfeu1	⊢ Ⅎ 𝑥 ∃! 𝑥 𝜑
2		nfab1	⊢ Ⅎ 𝑥 { 𝑥 ∣ 𝜑 }
3		nfiota1	⊢ Ⅎ 𝑥 ( ℩ 𝑥 𝜑 )
4	3	nfsn	⊢ Ⅎ 𝑥 { ( ℩ 𝑥 𝜑 ) }
5		iota1	⊢ ( ∃! 𝑥 𝜑 → ( 𝜑 ↔ ( ℩ 𝑥 𝜑 ) = 𝑥 ) )
6		eqcom	⊢ ( ( ℩ 𝑥 𝜑 ) = 𝑥 ↔ 𝑥 = ( ℩ 𝑥 𝜑 ) )
7	5 6	bitrdi	⊢ ( ∃! 𝑥 𝜑 → ( 𝜑 ↔ 𝑥 = ( ℩ 𝑥 𝜑 ) ) )
8		abid	⊢ ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜑 )
9		velsn	⊢ ( 𝑥 ∈ { ( ℩ 𝑥 𝜑 ) } ↔ 𝑥 = ( ℩ 𝑥 𝜑 ) )
10	7 8 9	3bitr4g	⊢ ( ∃! 𝑥 𝜑 → ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑥 ∈ { ( ℩ 𝑥 𝜑 ) } ) )
11	1 2 4 10	eqrd	⊢ ( ∃! 𝑥 𝜑 → { 𝑥 ∣ 𝜑 } = { ( ℩ 𝑥 𝜑 ) } )