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

Metamath Proof Explorer

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 eqtrid ⊢ ( 𝐴 ∈ 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 ( 𝜓 , { 𝐴 } , ∅ )