Metamath Proof Explorer

Theorem ab0

Description: The class of sets verifying a property is the empty class if and only if that property is a contradiction. See also abn0 (from which it could be proved using as many essential proof steps but one fewer syntactic step, at the cost of depending on df-ne ). (Contributed by BJ, 19-Mar-2021) Avoid df-clel , ax-8 . (Revised by Gino Giotto, 30-Aug-2024)

Ref Expression
Assertion ab0 ⊢ x | φ = ∅ ↔ ∀ x ¬ φ

Proof

Step Hyp Ref Expression
1 dfnul4 ⊢ ∅ = x | ⊥
2 1 eqeq2i ⊢ x | φ = ∅ ↔ x | φ = x | ⊥
3 dfcleq ⊢ x | φ = x | ⊥ ↔ ∀ y y ∈ x | φ ↔ y ∈ x | ⊥
4 df-clab ⊢ y ∈ x | φ ↔ y x φ
5 sb6 ⊢ y x φ ↔ ∀ x x = y → φ
6 4 5 bitri ⊢ y ∈ x | φ ↔ ∀ x x = y → φ
7 df-clab ⊢ y ∈ x | ⊥ ↔ y x ⊥
8 sbv ⊢ y x ⊥ ↔ ⊥
9 7 8 bitri ⊢ y ∈ x | ⊥ ↔ ⊥
10 6 9 bibi12i ⊢ y ∈ x | φ ↔ y ∈ x | ⊥ ↔ ∀ x x = y → φ ↔ ⊥
11 10 albii ⊢ ∀ y y ∈ x | φ ↔ y ∈ x | ⊥ ↔ ∀ y ∀ x x = y → φ ↔ ⊥
12 nbfal ⊢ ¬ ∀ x x = y → φ ↔ ∀ x x = y → φ ↔ ⊥
13 12 bicomi ⊢ ∀ x x = y → φ ↔ ⊥ ↔ ¬ ∀ x x = y → φ
14 13 albii ⊢ ∀ y ∀ x x = y → φ ↔ ⊥ ↔ ∀ y ¬ ∀ x x = y → φ
15 nfna1 ⊢ Ⅎ x ¬ ∀ x x = y → φ
16 nfv ⊢ Ⅎ y ¬ φ
17 pm2.27 ⊢ x = y → x = y → φ → φ
18 17 spsd ⊢ x = y → ∀ x x = y → φ → φ
19 18 equcoms ⊢ y = x → ∀ x x = y → φ → φ
20 ax12v ⊢ x = y → φ → ∀ x x = y → φ
21 20 equcoms ⊢ y = x → φ → ∀ x x = y → φ
22 19 21 impbid ⊢ y = x → ∀ x x = y → φ ↔ φ
23 22 notbid ⊢ y = x → ¬ ∀ x x = y → φ ↔ ¬ φ
24 15 16 23 cbvalv1 ⊢ ∀ y ¬ ∀ x x = y → φ ↔ ∀ x ¬ φ
25 11 14 24 3bitri ⊢ ∀ y y ∈ x | φ ↔ y ∈ x | ⊥ ↔ ∀ x ¬ φ
26 2 3 25 3bitri ⊢ x | φ = ∅ ↔ ∀ x ¬ φ