Metamath Proof Explorer

Theorem rab0OLD

Description: Obsolete version of rab0 as of 10-Jun-2026. (Contributed by NM, 15-Oct-2003) (Proof shortened by Andrew Salmon, 26-Jun-2011) (Proof shortened by JJ, 14-Jul-2021) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion rab0OLD ⊢ 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 ∈ ∅ | φ = ∅