This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem r19.30

Description: Restricted quantifier version of 19.30 . (Contributed by Scott Fenton, 25-Feb-2011) (Proof shortened by Wolf Lammen, 5-Nov-2024)

Ref Expression
Assertion r19.30 ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ∨ 𝜓 ) → ( ∀ 𝑥 ∈ 𝐴 𝜑 ∨ ∃ 𝑥 ∈ 𝐴 𝜓 ) )

Proof

Step Hyp Ref Expression
1 pm2.53 ⊢ ( ( 𝜑 ∨ 𝜓 ) → ( ¬ 𝜑 → 𝜓 ) )
2 1 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ∨ 𝜓 ) → ∀ 𝑥 ∈ 𝐴 ( ¬ 𝜑 → 𝜓 ) )
3 rexnal ⊢ ( ∃ 𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∀ 𝑥 ∈ 𝐴 𝜑 )
4 3 biimpri ⊢ ( ¬ ∀ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑥 ∈ 𝐴 ¬ 𝜑 )
5 rexim ⊢ ( ∀ 𝑥 ∈ 𝐴 ( ¬ 𝜑 → 𝜓 ) → ( ∃ 𝑥 ∈ 𝐴 ¬ 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜓 ) )
6 2 4 5 syl2im ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ∨ 𝜓 ) → ( ¬ ∀ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜓 ) )
7 6 orrd ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ∨ 𝜓 ) → ( ∀ 𝑥 ∈ 𝐴 𝜑 ∨ ∃ 𝑥 ∈ 𝐴 𝜓 ) )