Theorem rabsnt

Description: Truth implied by equality of a restricted class abstraction and a singleton. (Contributed by NM, 29-May-2006) (Proof shortened by Mario Carneiro, 23-Dec-2016)

	Ref	Expression
Hypotheses	rabsnt.1	|- B e. _V
	rabsnt.2	|- ( x = B -> ( ph <-> ps ) )
Assertion	rabsnt	|- ( { x e. A | ph } = { B } -> ps )

Proof

Step	Hyp	Ref	Expression
1		rabsnt.1	|- B e. _V
2		rabsnt.2	|- ( x = B -> ( ph <-> ps ) )
3	1	snid	|- B e. { B }
4		id	|- ( { x e. A | ph } = { B } -> { x e. A | ph } = { B } )
5	3 4	eleqtrrid	|- ( { x e. A | ph } = { B } -> B e. { x e. A | ph } )
6	2	elrab	|- ( B e. { x e. A | ph } <-> ( B e. A /\ ps ) )
7	6	simprbi	|- ( B e. { x e. A | ph } -> ps )
8	5 7	syl	|- ( { x e. A | ph } = { B } -> ps )