Metamath Proof Explorer

Theorem ab0w

Description: The class of sets verifying a property is the empty class if and only if that property is a contradiction. Version of ab0 using implicit substitution, which requires fewer axioms. (Contributed by GG, 3-Oct-2024)

Ref Expression
Hypothesis ab0w.1 ⊢ x = y → φ ↔ ψ
Assertion ab0w ⊢ x | φ = ∅ ↔ ∀ y ¬ ψ

Proof

Step Hyp Ref Expression
1 ab0w.1 ⊢ x = y → φ ↔ ψ
2 dfnul4 ⊢ ∅ = x | ⊥
3 2 eqeq2i ⊢ x | φ = ∅ ↔ x | φ = x | ⊥
4 dfcleq ⊢ x | φ = x | ⊥ ↔ ∀ y y ∈ x | φ ↔ y ∈ x | ⊥
5 df-clab ⊢ y ∈ x | φ ↔ y x φ
6 1 sbievw ⊢ y x φ ↔ ψ
7 5 6 bitri ⊢ y ∈ x | φ ↔ ψ
8 7 bibi1i ⊢ y ∈ x | φ ↔ y ∈ x | ⊥ ↔ ψ ↔ y ∈ x | ⊥
9 bicom ⊢ ψ ↔ y ∈ x | ⊥ ↔ y ∈ x | ⊥ ↔ ψ
10 8 9 bitri ⊢ y ∈ x | φ ↔ y ∈ x | ⊥ ↔ y ∈ x | ⊥ ↔ ψ
11 10 albii ⊢ ∀ y y ∈ x | φ ↔ y ∈ x | ⊥ ↔ ∀ y y ∈ x | ⊥ ↔ ψ
12 4 11 bitri ⊢ x | φ = x | ⊥ ↔ ∀ y y ∈ x | ⊥ ↔ ψ
13 df-clab ⊢ y ∈ x | ⊥ ↔ y x ⊥
14 sbv ⊢ y x ⊥ ↔ ⊥
15 13 14 bitri ⊢ y ∈ x | ⊥ ↔ ⊥
16 15 bibi1i ⊢ y ∈ x | ⊥ ↔ ψ ↔ ⊥ ↔ ψ
17 16 albii ⊢ ∀ y y ∈ x | ⊥ ↔ ψ ↔ ∀ y ⊥ ↔ ψ
18 falim ⊢ ⊥ → ψ → ¬ ψ
19 idd ⊢ ¬ ⊥ → ¬ ψ → ¬ ψ
20 18 19 bija ⊢ ⊥ ↔ ψ → ¬ ψ
21 falim ⊢ ⊥ → ψ
22 id ⊢ ψ → ψ
23 21 22 pm5.21ni ⊢ ¬ ψ → ⊥ ↔ ψ
24 20 23 impbii ⊢ ⊥ ↔ ψ ↔ ¬ ψ
25 24 albii ⊢ ∀ y ⊥ ↔ ψ ↔ ∀ y ¬ ψ
26 17 25 bitri ⊢ ∀ y y ∈ x | ⊥ ↔ ψ ↔ ∀ y ¬ ψ
27 12 26 bitri ⊢ x | φ = x | ⊥ ↔ ∀ y ¬ ψ
28 3 27 bitri ⊢ x | φ = ∅ ↔ ∀ y ¬ ψ