Theorem absneu

Description: Restricted existential uniqueness determined by a singleton. (Contributed by NM, 29-May-2006)

	Ref	Expression
Assertion	absneu	⊢ ( ( 𝐴 ∈ 𝑉 ∧ { 𝑥 ∣ 𝜑 } = { 𝐴 } ) → ∃! 𝑥 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		sneq	⊢ ( 𝑦 = 𝐴 → { 𝑦 } = { 𝐴 } )
2	1	eqeq2d	⊢ ( 𝑦 = 𝐴 → ( { 𝑥 ∣ 𝜑 } = { 𝑦 } ↔ { 𝑥 ∣ 𝜑 } = { 𝐴 } ) )
3	2	spcegv	⊢ ( 𝐴 ∈ 𝑉 → ( { 𝑥 ∣ 𝜑 } = { 𝐴 } → ∃ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } ) )
4	3	imp	⊢ ( ( 𝐴 ∈ 𝑉 ∧ { 𝑥 ∣ 𝜑 } = { 𝐴 } ) → ∃ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } )
5		euabsn2	⊢ ( ∃! 𝑥 𝜑 ↔ ∃ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } )
6	4 5	sylibr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ { 𝑥 ∣ 𝜑 } = { 𝐴 } ) → ∃! 𝑥 𝜑 )