Theorem rabsnel

Description: Truth implied by equality of a restricted class abstraction and a singleton. (Contributed by Thierry Arnoux, 15-Sep-2018)

	Ref	Expression
Hypothesis	rabsnel.1	|- B e. _V
Assertion	rabsnel	|- ( { x e. A | ph } = { B } -> B e. A )

Proof

Step	Hyp	Ref	Expression
1		rabsnel.1	|- B e. _V
2	1	snid	|- B e. { B }
3		eleq2	|- ( { x e. A | ph } = { B } -> ( B e. { x e. A | ph } <-> B e. { B } ) )
4	2 3	mpbiri	|- ( { x e. A | ph } = { B } -> B e. { x e. A | ph } )
5		elrabi	|- ( B e. { x e. A | ph } -> B e. A )
6	4 5	syl	|- ( { x e. A | ph } = { B } -> B e. A )