Metamath Proof Explorer

Theorem ralf0

Description: The quantification of a falsehood is vacuous when true. (Contributed by NM, 26-Nov-2005) (Proof shortened by JJ, 14-Jul-2021) Avoid df-clel , ax-8 . (Revised by Gino Giotto, 2-Sep-2024)

Ref Expression
Hypothesis ralf0.1 ⊢ ¬ φ
Assertion ralf0 ⊢ ∀ x ∈ A φ ↔ A = ∅

Proof

Step Hyp Ref Expression
1 ralf0.1 ⊢ ¬ φ
2 r19.26 ⊢ ∀ x ∈ A ¬ φ ∧ φ ↔ ∀ x ∈ A ¬ φ ∧ ∀ x ∈ A φ
3 pm2.24 ⊢ φ → ¬ φ → ⊥
4 3 impcom ⊢ ¬ φ ∧ φ → ⊥
5 4 ralimi ⊢ ∀ x ∈ A ¬ φ ∧ φ → ∀ x ∈ A ⊥
6 df-ral ⊢ ∀ x ∈ A ⊥ ↔ ∀ x x ∈ A → ⊥
7 dfnot ⊢ ¬ x ∈ A ↔ x ∈ A → ⊥
8 7 bicomi ⊢ x ∈ A → ⊥ ↔ ¬ x ∈ A
9 8 albii ⊢ ∀ x x ∈ A → ⊥ ↔ ∀ x ¬ x ∈ A
10 6 9 sylbb ⊢ ∀ x ∈ A ⊥ → ∀ x ¬ x ∈ A
11 id ⊢ x ∈ A → x ∈ A
12 falim ⊢ ⊥ → x ∈ A
13 11 12 pm5.21ni ⊢ ¬ x ∈ A → x ∈ A ↔ ⊥
14 df-clab ⊢ x ∈ y | ⊥ ↔ x y ⊥
15 sbv ⊢ x y ⊥ ↔ ⊥
16 14 15 bitri ⊢ x ∈ y | ⊥ ↔ ⊥
17 13 16 bitr4di ⊢ ¬ x ∈ A → x ∈ A ↔ x ∈ y | ⊥
18 17 alimi ⊢ ∀ x ¬ x ∈ A → ∀ x x ∈ A ↔ x ∈ y | ⊥
19 dfcleq ⊢ A = y | ⊥ ↔ ∀ x x ∈ A ↔ x ∈ y | ⊥
20 18 19 sylibr ⊢ ∀ x ¬ x ∈ A → A = y | ⊥
21 dfnul4 ⊢ ∅ = y | ⊥
22 20 21 eqtr4di ⊢ ∀ x ¬ x ∈ A → A = ∅
23 5 10 22 3syl ⊢ ∀ x ∈ A ¬ φ ∧ φ → A = ∅
24 2 23 sylbir ⊢ ∀ x ∈ A ¬ φ ∧ ∀ x ∈ A φ → A = ∅
25 24 ex ⊢ ∀ x ∈ A ¬ φ → ∀ x ∈ A φ → A = ∅
26 1 a1i ⊢ x ∈ A → ¬ φ
27 25 26 mprg ⊢ ∀ x ∈ A φ → A = ∅
28 rzal ⊢ A = ∅ → ∀ x ∈ A φ
29 27 28 impbii ⊢ ∀ x ∈ A φ ↔ A = ∅