Theorem rabsn

Description: Condition where a restricted class abstraction is a singleton. (Contributed by NM, 28-May-2006) (Proof shortened by AV, 26-Aug-2022)

	Ref	Expression
Assertion	rabsn	⊢ ( 𝐵 ∈ 𝐴 → { 𝑥 ∈ 𝐴 ∣ 𝑥 = 𝐵 } = { 𝐵 } )

Proof

Step	Hyp	Ref	Expression
1		eleq1	⊢ ( 𝑥 = 𝐵 → ( 𝑥 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴 ) )
2	1	pm5.32ri	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 = 𝐵 ) ↔ ( 𝐵 ∈ 𝐴 ∧ 𝑥 = 𝐵 ) )
3	2	baib	⊢ ( 𝐵 ∈ 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 = 𝐵 ) ↔ 𝑥 = 𝐵 ) )
4	3	alrimiv	⊢ ( 𝐵 ∈ 𝐴 → ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 = 𝐵 ) ↔ 𝑥 = 𝐵 ) )
5		rabeqsn	⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝑥 = 𝐵 } = { 𝐵 } ↔ ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 = 𝐵 ) ↔ 𝑥 = 𝐵 ) )
6	4 5	sylibr	⊢ ( 𝐵 ∈ 𝐴 → { 𝑥 ∈ 𝐴 ∣ 𝑥 = 𝐵 } = { 𝐵 } )