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

Metamath Proof Explorer

Theorem rab0

Description: Any restricted class abstraction restricted to the empty set is empty. (Contributed by NM, 15-Oct-2003) (Proof shortened by Andrew Salmon, 26-Jun-2011) (Proof shortened by JJ, 14-Jul-2021)

Ref Expression
Assertion rab0 ⊢ x ∈ ∅ | φ = ∅

Proof

Step Hyp Ref Expression
1 df-rab ⊢ x ∈ ∅ | φ = x | x ∈ ∅ ∧ φ
2 ab0 ⊢ x | x ∈ ∅ ∧ φ = ∅ ↔ ∀ x ¬ x ∈ ∅ ∧ φ
3 noel ⊢ ¬ x ∈ ∅
4 3 intnanr ⊢ ¬ x ∈ ∅ ∧ φ
5 2 4 mpgbir ⊢ x | x ∈ ∅ ∧ φ = ∅
6 1 5 eqtri ⊢ x ∈ ∅ | φ = ∅