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 Glauco Siliprandi, 24-Jan-2025)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | r19.28zf.1 | ⊢ Ⅎ 𝑥 𝜑 | |
| r19.28zf.2 | ⊢ Ⅎ 𝑥 𝐴 | ||
| Assertion | r19.28zf | ⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | r19.28zf.1 | ⊢ Ⅎ 𝑥 𝜑 | |
| 2 | r19.28zf.2 | ⊢ Ⅎ 𝑥 𝐴 | |
| 3 | r19.26 | ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ) | |
| 4 | 1 2 | r19.3rzf | ⊢ ( 𝐴 ≠ ∅ → ( 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 𝜑 ) ) |
| 5 | 4 | anbi1d | ⊢ ( 𝐴 ≠ ∅ → ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ) ) |
| 6 | 3 5 | bitr4id | ⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ) ) |