Metamath Proof Explorer


Theorem r19.28z

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 ( 𝐴 ≠ ∅ → ( ∀ 𝑥𝐴 ( 𝜑𝜓 ) ↔ ( 𝜑 ∧ ∀ 𝑥𝐴 𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 r19.3rz.1 𝑥 𝜑
2 r19.26 ( ∀ 𝑥𝐴 ( 𝜑𝜓 ) ↔ ( ∀ 𝑥𝐴 𝜑 ∧ ∀ 𝑥𝐴 𝜓 ) )
3 1 r19.3rz ( 𝐴 ≠ ∅ → ( 𝜑 ↔ ∀ 𝑥𝐴 𝜑 ) )
4 3 anbi1d ( 𝐴 ≠ ∅ → ( ( 𝜑 ∧ ∀ 𝑥𝐴 𝜓 ) ↔ ( ∀ 𝑥𝐴 𝜑 ∧ ∀ 𝑥𝐴 𝜓 ) ) )
5 2 4 bitr4id ( 𝐴 ≠ ∅ → ( ∀ 𝑥𝐴 ( 𝜑𝜓 ) ↔ ( 𝜑 ∧ ∀ 𝑥𝐴 𝜓 ) ) )