Metamath Proof Explorer

Theorem r19.28zf

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 ⊢ Ⅎ x φ
r19.28zf.2 ⊢ Ⅎ _ x A
Assertion r19.28zf ⊢ A ≠ ∅ → ∀ x ∈ A φ ∧ ψ ↔ φ ∧ ∀ x ∈ A ψ

Proof

Step Hyp Ref Expression
1 r19.28zf.1 ⊢ Ⅎ x φ
2 r19.28zf.2 ⊢ Ⅎ _ x A
3 r19.26 ⊢ ∀ x ∈ A φ ∧ ψ ↔ ∀ x ∈ A φ ∧ ∀ x ∈ A ψ
4 1 2 r19.3rzf ⊢ A ≠ ∅ → φ ↔ ∀ x ∈ A φ
5 4 anbi1d ⊢ A ≠ ∅ → φ ∧ ∀ x ∈ A ψ ↔ ∀ x ∈ A φ ∧ ∀ x ∈ A ψ
6 3 5 bitr4id ⊢ A ≠ ∅ → ∀ x ∈ A φ ∧ ψ ↔ φ ∧ ∀ x ∈ A ψ