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 ( 𝑀 = { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } → ( 𝑀 = ∅ ∨ 𝑀 = { 𝐴 } ) )

Proof

Step Hyp Ref Expression
1 rabsnifsb ⊢ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = if ( [ 𝐴 / 𝑥 ] 𝜑 , { 𝐴 } , ∅ )
2 1 eqeq2i ⊢ ( 𝑀 = { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } ↔ 𝑀 = if ( [ 𝐴 / 𝑥 ] 𝜑 , { 𝐴 } , ∅ ) )
3 ifeqor ⊢ ( if ( [ 𝐴 / 𝑥 ] 𝜑 , { 𝐴 } , ∅ ) = { 𝐴 } ∨ if ( [ 𝐴 / 𝑥 ] 𝜑 , { 𝐴 } , ∅ ) = ∅ )
4 orcom ⊢ ( ( if ( [ 𝐴 / 𝑥 ] 𝜑 , { 𝐴 } , ∅ ) = { 𝐴 } ∨ if ( [ 𝐴 / 𝑥 ] 𝜑 , { 𝐴 } , ∅ ) = ∅ ) ↔ ( if ( [ 𝐴 / 𝑥 ] 𝜑 , { 𝐴 } , ∅ ) = ∅ ∨ if ( [ 𝐴 / 𝑥 ] 𝜑 , { 𝐴 } , ∅ ) = { 𝐴 } ) )
5 3 4 mpbi ⊢ ( if ( [ 𝐴 / 𝑥 ] 𝜑 , { 𝐴 } , ∅ ) = ∅ ∨ if ( [ 𝐴 / 𝑥 ] 𝜑 , { 𝐴 } , ∅ ) = { 𝐴 } )
6 eqeq1 ⊢ ( 𝑀 = if ( [ 𝐴 / 𝑥 ] 𝜑 , { 𝐴 } , ∅ ) → ( 𝑀 = ∅ ↔ if ( [ 𝐴 / 𝑥 ] 𝜑 , { 𝐴 } , ∅ ) = ∅ ) )
7 eqeq1 ⊢ ( 𝑀 = if ( [ 𝐴 / 𝑥 ] 𝜑 , { 𝐴 } , ∅ ) → ( 𝑀 = { 𝐴 } ↔ if ( [ 𝐴 / 𝑥 ] 𝜑 , { 𝐴 } , ∅ ) = { 𝐴 } ) )
8 6 7 orbi12d ⊢ ( 𝑀 = if ( [ 𝐴 / 𝑥 ] 𝜑 , { 𝐴 } , ∅ ) → ( ( 𝑀 = ∅ ∨ 𝑀 = { 𝐴 } ) ↔ ( if ( [ 𝐴 / 𝑥 ] 𝜑 , { 𝐴 } , ∅ ) = ∅ ∨ if ( [ 𝐴 / 𝑥 ] 𝜑 , { 𝐴 } , ∅ ) = { 𝐴 } ) ) )
9 5 8 mpbiri ⊢ ( 𝑀 = if ( [ 𝐴 / 𝑥 ] 𝜑 , { 𝐴 } , ∅ ) → ( 𝑀 = ∅ ∨ 𝑀 = { 𝐴 } ) )
10 2 9 sylbi ⊢ ( 𝑀 = { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } → ( 𝑀 = ∅ ∨ 𝑀 = { 𝐴 } ) )