This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )