Metamath Proof Explorer

Theorem ab0OLD

Description: Obsolete version of ab0 as of 8-Sep-2024. (Contributed by BJ, 19-Mar-2021) Avoid df-clel , ax-8 . (Revised by Gino Giotto, 30-Aug-2024) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

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