Metamath Proof Explorer

Theorem eq0rdv

Description: Deduction for equality to the empty set. (Contributed by NM, 11-Jul-2014) Avoid ax-8 , df-clel . (Revised by Gino Giotto, 6-Sep-2024)

Ref Expression
Hypothesis eq0rdv.1 ⊢ φ → ¬ x ∈ A
Assertion eq0rdv ⊢ φ → A = ∅

Proof

Step Hyp Ref Expression
1 eq0rdv.1 ⊢ φ → ¬ x ∈ A
2 1 alrimiv ⊢ φ → ∀ x ¬ x ∈ A
3 dfnul4 ⊢ ∅ = y | ⊥
4 3 eqeq2i ⊢ A = ∅ ↔ A = y | ⊥
5 dfcleq ⊢ A = y | ⊥ ↔ ∀ x x ∈ A ↔ x ∈ y | ⊥
6 df-clab ⊢ x ∈ y | ⊥ ↔ x y ⊥
7 sbv ⊢ x y ⊥ ↔ ⊥
8 6 7 bitri ⊢ x ∈ y | ⊥ ↔ ⊥
9 8 bibi2i ⊢ x ∈ A ↔ x ∈ y | ⊥ ↔ x ∈ A ↔ ⊥
10 9 albii ⊢ ∀ x x ∈ A ↔ x ∈ y | ⊥ ↔ ∀ x x ∈ A ↔ ⊥
11 nbfal ⊢ ¬ x ∈ A ↔ x ∈ A ↔ ⊥
12 11 bicomi ⊢ x ∈ A ↔ ⊥ ↔ ¬ x ∈ A
13 12 albii ⊢ ∀ x x ∈ A ↔ ⊥ ↔ ∀ x ¬ x ∈ A
14 10 13 bitri ⊢ ∀ x x ∈ A ↔ x ∈ y | ⊥ ↔ ∀ x ¬ x ∈ A
15 4 5 14 3bitrri ⊢ ∀ x ¬ x ∈ A ↔ A = ∅
16 2 15 sylib ⊢ φ → A = ∅