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 GG, 2-Sep-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | rzal | ⊢ ( 𝐴 = ∅ → ∀ 𝑥 ∈ 𝐴 𝜑 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | biidd | ⊢ ( 𝑦 = 𝑥 → ( ⊥ ↔ ⊥ ) ) | |
| 2 | 1 | eqabbw | ⊢ ( 𝐴 = { 𝑦 ∣ ⊥ } ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ⊥ ) ) |
| 3 | 2 | biimpi | ⊢ ( 𝐴 = { 𝑦 ∣ ⊥ } → ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ⊥ ) ) |
| 4 | nbfal | ⊢ ( ¬ 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐴 ↔ ⊥ ) ) | |
| 5 | pm2.21 | ⊢ ( ¬ 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 → 𝜑 ) ) | |
| 6 | 4 5 | sylbir | ⊢ ( ( 𝑥 ∈ 𝐴 ↔ ⊥ ) → ( 𝑥 ∈ 𝐴 → 𝜑 ) ) |
| 7 | 3 6 | sylg | ⊢ ( 𝐴 = { 𝑦 ∣ ⊥ } → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) |
| 8 | dfnul4 | ⊢ ∅ = { 𝑦 ∣ ⊥ } | |
| 9 | 8 | eqeq2i | ⊢ ( 𝐴 = ∅ ↔ 𝐴 = { 𝑦 ∣ ⊥ } ) |
| 10 | df-ral | ⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) | |
| 11 | 7 9 10 | 3imtr4i | ⊢ ( 𝐴 = ∅ → ∀ 𝑥 ∈ 𝐴 𝜑 ) |