Theorem rabsssn

Description: Conditions for a restricted class abstraction to be a subset of a singleton, i.e. to be a singleton or the empty set. (Contributed by AV, 18-Apr-2019)

	Ref	Expression
Assertion	rabsssn	|- ( { x e. V | ph } C_ { X } <-> A. x e. V ( ph -> x = X ) )

Proof

Step	Hyp	Ref	Expression
1		df-rab	|- { x e. V | ph } = { x | ( x e. V /\ ph ) }
2		df-sn	|- { X } = { x | x = X }
3	1 2	sseq12i	|- ( { x e. V | ph } C_ { X } <-> { x | ( x e. V /\ ph ) } C_ { x | x = X } )
4		ss2ab	|- ( { x | ( x e. V /\ ph ) } C_ { x | x = X } <-> A. x ( ( x e. V /\ ph ) -> x = X ) )
5		impexp	|- ( ( ( x e. V /\ ph ) -> x = X ) <-> ( x e. V -> ( ph -> x = X ) ) )
6	5	albii	|- ( A. x ( ( x e. V /\ ph ) -> x = X ) <-> A. x ( x e. V -> ( ph -> x = X ) ) )
7		df-ral	|- ( A. x e. V ( ph -> x = X ) <-> A. x ( x e. V -> ( ph -> x = X ) ) )
8	6 7	bitr4i	|- ( A. x ( ( x e. V /\ ph ) -> x = X ) <-> A. x e. V ( ph -> x = X ) )
9	3 4 8	3bitri	|- ( { x e. V | ph } C_ { X } <-> A. x e. V ( ph -> x = X ) )