Metamath Proof Explorer


Theorem r19.37zv

Description: Restricted quantifier version of Theorem 19.37 of Margaris p. 90. It is valid only when the domain of quantification is not empty. (Contributed by Paul Chapman, 8-Oct-2007)

Ref Expression
Assertion r19.37zv ( 𝐴 ≠ ∅ → ( ∃ 𝑥𝐴 ( 𝜑𝜓 ) ↔ ( 𝜑 → ∃ 𝑥𝐴 𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 r19.35 ( ∃ 𝑥𝐴 ( 𝜑𝜓 ) ↔ ( ∀ 𝑥𝐴 𝜑 → ∃ 𝑥𝐴 𝜓 ) )
2 r19.3rzv ( 𝐴 ≠ ∅ → ( 𝜑 ↔ ∀ 𝑥𝐴 𝜑 ) )
3 2 imbi1d ( 𝐴 ≠ ∅ → ( ( 𝜑 → ∃ 𝑥𝐴 𝜓 ) ↔ ( ∀ 𝑥𝐴 𝜑 → ∃ 𝑥𝐴 𝜓 ) ) )
4 1 3 bitr4id ( 𝐴 ≠ ∅ → ( ∃ 𝑥𝐴 ( 𝜑𝜓 ) ↔ ( 𝜑 → ∃ 𝑥𝐴 𝜓 ) ) )