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 Gino Giotto, 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|⊥↔∀yy∈x|φ↔y∈x|⊥
5 df-clab ⊢y∈x|φ↔yxφ
6 1 sbievw ⊢yxφ↔ψ
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 ⊢∀yy∈x|φ↔y∈x|⊥↔∀yy∈x|⊥↔ψ
12 4 11 bitri ⊢x|φ=x|⊥↔∀yy∈x|⊥↔ψ
13 df-clab ⊢y∈x|⊥↔yx⊥
14 sbv ⊢yx⊥↔⊥
15 13 14 bitri ⊢y∈x|⊥↔⊥
16 15 bibi1i ⊢y∈x|⊥↔ψ↔⊥↔ψ
17 16 albii ⊢∀yy∈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 ⊢∀yy∈x|⊥↔ψ↔∀y¬ψ
27 12 26 bitri ⊢x|φ=x|⊥↔∀y¬ψ
28 3 27 bitri ⊢x|φ=∅↔∀y¬ψ