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	$$⊢B\in A\to \left\{x\in A|x=B\right\}=\left\{B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		eleq1	$$⊢x=B\to \left(x\in A\leftrightarrow B\in A\right)$$
2	1	pm5.32ri	$$⊢\left(x\in A\wedge x=B\right)\leftrightarrow \left(B\in A\wedge x=B\right)$$
3	2	baib	$$⊢B\in A\to \left(\left(x\in A\wedge x=B\right)\leftrightarrow x=B\right)$$
4	3	alrimiv	$$⊢B\in A\to \forall x\left(\left(x\in A\wedge x=B\right)\leftrightarrow x=B\right)$$
5		rabeqsn	$$⊢\left\{x\in A|x=B\right\}=\left\{B\right\}\leftrightarrow \forall x\left(\left(x\in A\wedge x=B\right)\leftrightarrow x=B\right)$$
6	4 5	sylibr	$$⊢B\in A\to \left\{x\in A|x=B\right\}=\left\{B\right\}$$