Metamath Proof Explorer

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 e. A -> { x e. A | x = B } = { B } )

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( x = B -> ( x e. A <-> B e. A ) )
2 1 pm5.32ri 
 |-  ( ( x e. A /\ x = B ) <-> ( B e. A /\ x = B ) )
3 2 baib 
 |-  ( B e. A -> ( ( x e. A /\ x = B ) <-> x = B ) )
4 3 alrimiv 
 |-  ( B e. A -> A. x ( ( x e. A /\ x = B ) <-> x = B ) )
5 rabeqsn 
 |-  ( { x e. A | x = B } = { B } <-> A. x ( ( x e. A /\ x = B ) <-> x = B ) )
6 4 5 sylibr 
 |-  ( B e. A -> { x e. A | x = B } = { B } )