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

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

Metamath Proof Explorer