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	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
Assertion	rabsnif	⊢ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = if ( 𝜓 , { 𝐴 } , ∅ )

Proof

Step	Hyp	Ref	Expression
1		rabsnif.f	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
2		rabsnifsb	⊢ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = if ( [ 𝐴 / 𝑥 ] 𝜑 , { 𝐴 } , ∅ )
3	1	sbcieg	⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝜓 ) )
4	3	ifbid	⊢ ( 𝐴 ∈ V → if ( [ 𝐴 / 𝑥 ] 𝜑 , { 𝐴 } , ∅ ) = if ( 𝜓 , { 𝐴 } , ∅ ) )
5	2 4	syl5eq	⊢ ( 𝐴 ∈ V → { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = if ( 𝜓 , { 𝐴 } , ∅ ) )
6		rab0	⊢ { 𝑥 ∈ ∅ ∣ 𝜑 } = ∅
7		ifid	⊢ if ( 𝜓 , ∅ , ∅ ) = ∅
8	6 7	eqtr4i	⊢ { 𝑥 ∈ ∅ ∣ 𝜑 } = if ( 𝜓 , ∅ , ∅ )
9		snprc	⊢ ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
10	9	biimpi	⊢ ( ¬ 𝐴 ∈ V → { 𝐴 } = ∅ )
11	10	rabeqdv	⊢ ( ¬ 𝐴 ∈ V → { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = { 𝑥 ∈ ∅ ∣ 𝜑 } )
12	10	ifeq1d	⊢ ( ¬ 𝐴 ∈ V → if ( 𝜓 , { 𝐴 } , ∅ ) = if ( 𝜓 , ∅ , ∅ ) )
13	8 11 12	3eqtr4a	⊢ ( ¬ 𝐴 ∈ V → { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = if ( 𝜓 , { 𝐴 } , ∅ ) )
14	5 13	pm2.61i	⊢ { 𝑥 ∈ { 𝐴 } ∣ 𝜑 } = if ( 𝜓 , { 𝐴 } , ∅ )