Theorem rabsnif

Description: A restricted class abstraction restricted to a singleton is either the empty set or the singleton itself. (Contributed by AV, 12-Apr-2019) (Proof shortened by AV, 21-Jul-2019)

	Ref	Expression
Hypothesis	rabsnif.f	|- ( x = A -> ( ph <-> ps ) )
Assertion	rabsnif	|- { x e. { A } | ph } = if ( ps , { A } , (/) )

Proof

Step	Hyp	Ref	Expression
1		rabsnif.f	|- ( x = A -> ( ph <-> ps ) )
2		rabsnifsb	|- { x e. { A } | ph } = if ( [. A / x ]. ph , { A } , (/) )
3	1	sbcieg	|- ( A e. _V -> ( [. A / x ]. ph <-> ps ) )
4	3	ifbid	|- ( A e. _V -> if ( [. A / x ]. ph , { A } , (/) ) = if ( ps , { A } , (/) ) )
5	2 4	eqtrid	|- ( A e. _V -> { x e. { A } | ph } = if ( ps , { A } , (/) ) )
6		rab0	|- { x e. (/) | ph } = (/)
7		ifid	|- if ( ps , (/) , (/) ) = (/)
8	6 7	eqtr4i	|- { x e. (/) | ph } = if ( ps , (/) , (/) )
9		snprc	|- ( -. A e. _V <-> { A } = (/) )
10	9	biimpi	|- ( -. A e. _V -> { A } = (/) )
11	10	rabeqdv	|- ( -. A e. _V -> { x e. { A } | ph } = { x e. (/) | ph } )
12	10	ifeq1d	|- ( -. A e. _V -> if ( ps , { A } , (/) ) = if ( ps , (/) , (/) ) )
13	8 11 12	3eqtr4a	|- ( -. A e. _V -> { x e. { A } | ph } = if ( ps , { A } , (/) ) )
14	5 13	pm2.61i	|- { x e. { A } | ph } = if ( ps , { A } , (/) )