Theorem rabsneu

Description: Restricted existential uniqueness determined by a singleton. (Contributed by NM, 29-May-2006) (Revised by Mario Carneiro, 23-Dec-2016)

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

Proof

Step	Hyp	Ref	Expression
1		df-rab	⊢ { 𝑥 ∈ 𝐵 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) }
2	1	eqeq1i	⊢ ( { 𝑥 ∈ 𝐵 ∣ 𝜑 } = { 𝐴 } ↔ { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) } = { 𝐴 } )
3		absneu	⊢ ( ( 𝐴 ∈ 𝑉 ∧ { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) } = { 𝐴 } ) → ∃! 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) )
4	2 3	sylan2b	⊢ ( ( 𝐴 ∈ 𝑉 ∧ { 𝑥 ∈ 𝐵 ∣ 𝜑 } = { 𝐴 } ) → ∃! 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) )
5		df-reu	⊢ ( ∃! 𝑥 ∈ 𝐵 𝜑 ↔ ∃! 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) )
6	4 5	sylibr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ { 𝑥 ∈ 𝐵 ∣ 𝜑 } = { 𝐴 } ) → ∃! 𝑥 ∈ 𝐵 𝜑 )