Theorem rabrsn

Description: A restricted class abstraction restricted to a singleton is either the empty set or the singleton itself. (Contributed by Alexander van der Vekens, 22-Dec-2017) (Proof shortened by AV, 21-Jul-2019)

	Ref	Expression
Assertion	rabrsn	|- ( M = { x e. { A } | ph } -> ( M = (/) \/ M = { A } ) )

Proof

Step	Hyp	Ref	Expression
1		rabsnifsb	|- { x e. { A } | ph } = if ( [. A / x ]. ph , { A } , (/) )
2	1	eqeq2i	|- ( M = { x e. { A } | ph } <-> M = if ( [. A / x ]. ph , { A } , (/) ) )
3		ifeqor	|- ( if ( [. A / x ]. ph , { A } , (/) ) = { A } \/ if ( [. A / x ]. ph , { A } , (/) ) = (/) )
4		orcom	|- ( ( if ( [. A / x ]. ph , { A } , (/) ) = { A } \/ if ( [. A / x ]. ph , { A } , (/) ) = (/) ) <-> ( if ( [. A / x ]. ph , { A } , (/) ) = (/) \/ if ( [. A / x ]. ph , { A } , (/) ) = { A } ) )
5	3 4	mpbi	|- ( if ( [. A / x ]. ph , { A } , (/) ) = (/) \/ if ( [. A / x ]. ph , { A } , (/) ) = { A } )
6		eqeq1	|- ( M = if ( [. A / x ]. ph , { A } , (/) ) -> ( M = (/) <-> if ( [. A / x ]. ph , { A } , (/) ) = (/) ) )
7		eqeq1	|- ( M = if ( [. A / x ]. ph , { A } , (/) ) -> ( M = { A } <-> if ( [. A / x ]. ph , { A } , (/) ) = { A } ) )
8	6 7	orbi12d	|- ( M = if ( [. A / x ]. ph , { A } , (/) ) -> ( ( M = (/) \/ M = { A } ) <-> ( if ( [. A / x ]. ph , { A } , (/) ) = (/) \/ if ( [. A / x ]. ph , { A } , (/) ) = { A } ) ) )
9	5 8	mpbiri	|- ( M = if ( [. A / x ]. ph , { A } , (/) ) -> ( M = (/) \/ M = { A } ) )
10	2 9	sylbi	|- ( M = { x e. { A } | ph } -> ( M = (/) \/ M = { A } ) )