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 ⊢ x = A → φ ↔ ψ
Assertion rabsnif ⊢ x ∈ A | φ = if ψ A ∅

Proof

Step Hyp Ref Expression
1 rabsnif.f ⊢ x = A → φ ↔ ψ
2 rabsnifsb ⊢ x ∈ A | φ = if [˙A / x]˙ φ A ∅
3 1 sbcieg ⊢ A ∈ V → [˙A / x]˙ φ ↔ ψ
4 3 ifbid ⊢ A ∈ V → if [˙A / x]˙ φ A ∅ = if ψ A ∅
5 2 4 eqtrid ⊢ A ∈ V → x ∈ A | φ = if ψ A ∅
6 rab0 ⊢ x ∈ ∅ | φ = ∅
7 ifid ⊢ if ψ ∅ ∅ = ∅
8 6 7 eqtr4i ⊢ x ∈ ∅ | φ = if ψ ∅ ∅
9 snprc ⊢ ¬ A ∈ V ↔ A = ∅
10 9 biimpi ⊢ ¬ A ∈ V → A = ∅
11 10 rabeqdv ⊢ ¬ A ∈ V → x ∈ A | φ = x ∈ ∅ | φ
12 10 ifeq1d ⊢ ¬ A ∈ V → if ψ A ∅ = if ψ ∅ ∅
13 8 11 12 3eqtr4a ⊢ ¬ A ∈ V → x ∈ A | φ = if ψ A ∅
14 5 13 pm2.61i ⊢ x ∈ A | φ = if ψ A ∅