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

Metamath Proof Explorer

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