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 ⊢ M = x ∈ A | φ → M = ∅ ∨ M = A

Proof

Step Hyp Ref Expression
1 rabsnifsb ⊢ x ∈ A | φ = if [˙A / x]˙ φ A ∅
2 1 eqeq2i ⊢ M = x ∈ A | φ ↔ M = if [˙A / x]˙ φ A ∅
3 ifeqor ⊢ if [˙A / x]˙ φ A ∅ = A ∨ if [˙A / x]˙ φ A ∅ = ∅
4 orcom ⊢ if [˙A / x]˙ φ A ∅ = A ∨ if [˙A / x]˙ φ A ∅ = ∅ ↔ if [˙A / x]˙ φ A ∅ = ∅ ∨ if [˙A / x]˙ φ A ∅ = A
5 3 4 mpbi ⊢ if [˙A / x]˙ φ A ∅ = ∅ ∨ if [˙A / x]˙ φ A ∅ = A
6 eqeq1 ⊢ M = if [˙A / x]˙ φ A ∅ → M = ∅ ↔ if [˙A / x]˙ φ A ∅ = ∅
7 eqeq1 ⊢ M = if [˙A / x]˙ φ A ∅ → M = A ↔ if [˙A / x]˙ φ A ∅ = A
8 6 7 orbi12d ⊢ M = if [˙A / x]˙ φ A ∅ → M = ∅ ∨ M = A ↔ if [˙A / x]˙ φ A ∅ = ∅ ∨ if [˙A / x]˙ φ A ∅ = A
9 5 8 mpbiri ⊢ M = if [˙A / x]˙ φ A ∅ → M = ∅ ∨ M = A
10 2 9 sylbi ⊢ M = x ∈ A | φ → M = ∅ ∨ M = A