Description: Restricted quantifier version of Theorem 19.3 of Margaris p. 89. We don't need the nonempty class condition of r19.3rzv when there is an outer quantifier. (Contributed by NM, 25-Oct-2012)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | rr19.3v | ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 𝜑 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | biidd | ⊢ ( 𝑦 = 𝑥 → ( 𝜑 ↔ 𝜑 ) ) | |
| 2 | 1 | rspcv | ⊢ ( 𝑥 ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝐴 𝜑 → 𝜑 ) ) |
| 3 | 2 | ralimia | ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑 → ∀ 𝑥 ∈ 𝐴 𝜑 ) |
| 4 | ax-1 | ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 → 𝜑 ) ) | |
| 5 | 4 | ralrimiv | ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐴 𝜑 ) |
| 6 | 5 | ralimi | ⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑 ) |
| 7 | 3 6 | impbii | ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 𝜑 ) |