Metamath Proof Explorer

Theorem rzal

Description: Vacuous quantification is always true. (Contributed by NM, 11-Mar-1997) (Proof shortened by Andrew Salmon, 26-Jun-2011) Avoid df-clel , ax-8 . (Revised by Gino Giotto, 2-Sep-2024)

Ref Expression
Assertion rzal ⊢ A = ∅ → ∀ x ∈ A φ

Proof

Step Hyp Ref Expression
1 dfcleq ⊢ A = y | ⊥ ↔ ∀ x x ∈ A ↔ x ∈ y | ⊥
2 1 biimpi ⊢ A = y | ⊥ → ∀ x x ∈ A ↔ x ∈ y | ⊥
3 df-clab ⊢ x ∈ y | ⊥ ↔ x y ⊥
4 sbv ⊢ x y ⊥ ↔ ⊥
5 3 4 bitri ⊢ x ∈ y | ⊥ ↔ ⊥
6 5 bibi2i ⊢ x ∈ A ↔ x ∈ y | ⊥ ↔ x ∈ A ↔ ⊥
7 nbfal ⊢ ¬ x ∈ A ↔ x ∈ A ↔ ⊥
8 pm2.21 ⊢ ¬ x ∈ A → x ∈ A → φ
9 7 8 sylbir ⊢ x ∈ A ↔ ⊥ → x ∈ A → φ
10 6 9 sylbi ⊢ x ∈ A ↔ x ∈ y | ⊥ → x ∈ A → φ
11 2 10 sylg ⊢ A = y | ⊥ → ∀ x x ∈ A → φ
12 dfnul4 ⊢ ∅ = y | ⊥
13 12 eqeq2i ⊢ A = ∅ ↔ A = y | ⊥
14 df-ral ⊢ ∀ x ∈ A φ ↔ ∀ x x ∈ A → φ
15 11 13 14 3imtr4i ⊢ A = ∅ → ∀ x ∈ A φ