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 df-clab ⊢ y ∈ x | ⊥ ↔ y x ⊥
5 sbv ⊢ y x ⊥ ↔ ⊥
6 4 5 bitri ⊢ y ∈ x | ⊥ ↔ ⊥
7 6 bibi2i ⊢ ψ ↔ y ∈ x | ⊥ ↔ ψ ↔ ⊥
8 7 albii ⊢ ∀ y ψ ↔ y ∈ x | ⊥ ↔ ∀ y ψ ↔ ⊥
9 1 eqabcbw ⊢ x | φ = x | ⊥ ↔ ∀ y ψ ↔ y ∈ x | ⊥
10 nbfal ⊢ ¬ ψ ↔ ψ ↔ ⊥
11 10 albii ⊢ ∀ y ¬ ψ ↔ ∀ y ψ ↔ ⊥
12 8 9 11 3bitr4i ⊢ x | φ = x | ⊥ ↔ ∀ y ¬ ψ
13 3 12 bitri ⊢ x | φ = ∅ ↔ ∀ y ¬ ψ