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