Theorem euabsn

Description: Another way to express existential uniqueness of a wff: its class abstraction is a singleton. (Contributed by NM, 22-Feb-2004)

	Ref	Expression
Assertion	euabsn	⊢ ( ∃! 𝑥 𝜑 ↔ ∃ 𝑥 { 𝑥 ∣ 𝜑 } = { 𝑥 } )

Proof

Step	Hyp	Ref	Expression
1		euabsn2	⊢ ( ∃! 𝑥 𝜑 ↔ ∃ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } )
2		nfv	⊢ Ⅎ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑥 }
3		nfab1	⊢ Ⅎ 𝑥 { 𝑥 ∣ 𝜑 }
4	3	nfeq1	⊢ Ⅎ 𝑥 { 𝑥 ∣ 𝜑 } = { 𝑦 }
5		sneq	⊢ ( 𝑥 = 𝑦 → { 𝑥 } = { 𝑦 } )
6	5	eqeq2d	⊢ ( 𝑥 = 𝑦 → ( { 𝑥 ∣ 𝜑 } = { 𝑥 } ↔ { 𝑥 ∣ 𝜑 } = { 𝑦 } ) )
7	2 4 6	cbvexv1	⊢ ( ∃ 𝑥 { 𝑥 ∣ 𝜑 } = { 𝑥 } ↔ ∃ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } )
8	1 7	bitr4i	⊢ ( ∃! 𝑥 𝜑 ↔ ∃ 𝑥 { 𝑥 ∣ 𝜑 } = { 𝑥 } )