Theorem rabeqsn

Description: Conditions for a restricted class abstraction to be a singleton. (Contributed by AV, 18-Apr-2019) (Proof shortened by AV, 26-Aug-2022)

	Ref	Expression
Assertion	rabeqsn	|- ( { x e. V | ph } = { X } <-> A. x ( ( x e. V /\ ph ) <-> x = X ) )

Proof

Step	Hyp	Ref	Expression
1		df-rab	|- { x e. V | ph } = { x | ( x e. V /\ ph ) }
2	1	eqeq1i	|- ( { x e. V | ph } = { X } <-> { x | ( x e. V /\ ph ) } = { X } )
3		absn	|- ( { x | ( x e. V /\ ph ) } = { X } <-> A. x ( ( x e. V /\ ph ) <-> x = X ) )
4	2 3	bitri	|- ( { x e. V | ph } = { X } <-> A. x ( ( x e. V /\ ph ) <-> x = X ) )