Description: Restricted quantifier version of Theorem 19.28 of Margaris p. 90. It is valid only when the domain of quantification is not empty. (Contributed by NM, 26-Oct-2010)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | r19.3rz.1 | ⊢ Ⅎ 𝑥 𝜑 | |
| Assertion | r19.28z | ⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | r19.3rz.1 | ⊢ Ⅎ 𝑥 𝜑 | |
| 2 | r19.26 | ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ) | |
| 3 | 1 | r19.3rz | ⊢ ( 𝐴 ≠ ∅ → ( 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 𝜑 ) ) |
| 4 | 3 | anbi1d | ⊢ ( 𝐴 ≠ ∅ → ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ) ) |
| 5 | 2 4 | bitr4id | ⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ) ) |